book集

section 順序対

subsection 順序対
word \pr
abbr pr
br
word ◁ ▷
prop ◁.
prop ▷.
prop/thm pr:0 ◀ W.
prf pr:0 -| ◁. ,, ▷. p; pr:0 -| W. h;
br
txt 次のwordは一般的には \({\rm dom}\) \({\rm im}\)
word ^◁ ^▷
prop ^◁.
prop ^▷.

subsection 直積、関係
word ^^pr_
prop ^^pr_.
word ^^pr
prop ^^pr.
thm `[^^pr] {**}=_ [{^^}\pr]` ◀ W.
prf goal // W. -| O p; goal -| W. h;
br
word Rel
prop Rel.
prop/thm Rel.' ◀ W.
prf Rel.' /// W.!=. -| O p; Rel.' -| W. h;
prop/thm Rel.. ◀ W.
prf Rel.. -| ◁. ,, ▷. p; Rel.. -| W. h;
thm `R ∈_ Rel ⟹ ^◁ (R) =_ \; {^}◁ \! (R) and ^▷ (R) =_ \; {^}▷ \! (R)` ◀ W.
prf goal / W.!=. -| ◁. ,, ▷. {Rel..} p; goal -| W. h;

subsection 代入
word ^◁!
prop ^◁!.
br
word* ap
prop ap.
prop/thm ap:0 ◀ W.
prf ap:0 -| ap. p; ap:0 -| W. h;
br
word* *^ap
prop *^ap.
prop/thm *^ap:0 ◀ W.
prf *^ap:0 / W.!=. -| O p; *^ap:0 -| W. h;

subsection 対の入れ替え、逆関係
word sw
prop sw.
prop/thm sw:I ◀ W.
prf sw:I / sw. -| O p; sw:I -| W. h;
br
txt 次のwordは一般的には \(^{-1}\)
word ^sw
prop ^sw.
prop/thm ^sw:0 ◀ W.
prf ^sw:0 // W. -| sw. p; ^sw:0 -| W. h;
prop/thm ^sw:I ◀ W.
prf ^sw:I /2 =. // ^sw. -| sw:I p; ^sw:I -| W. h;

subsection 関係の合成
word ∘
prop ∘.
prop/thm ∘:0 ◀ W.
prf ∘:0 // W.!=. -| pr:0 p; ∘:0 -| W. h;
prop/thm ∘:A ◀ W.
prf ∘:A / =. // ∘. -| ◁. ,, ▷. p; ∘:A -| W. h;
prop/thm ∘:X ◀ W.
prf ∘:X /2 =. // W.!=. -| sw. p; ∘:X -| W. h;
prop/thm ∘ap ◀ W.
prf ∘ap -| ap:0 ,, ∘. ,, pr:0 ,, ^◁!. p; ∘ap -| W. h;
thm `(℘ (X ^^pr X) , [∘]) :2&:A` ◀ W.
prf goal / ℘. [&l -| ∘:0 || &r // W.!=. -| ∘:A] p; goal -| W. h;

newpage
section 写像

subsection 写像の集合
word →_
prop →_.
!prop/thm →_.' ◀ W.
prf →_.' // W.!=. -| O {Y_.-} p; →_.' -| W. h;
word →
prop →.
!prop/thm →.' ◀ W.
prf →.' / →. -| O {→_.'} p; →.' -| W. h;
thm `[ chain f ∈_ X →_ 𝕍 ⟺ f ∈ X → ^▷ (f) ⟺ ∃ Y f ∈ X → Y ]` ◀ W.
prf goal / W.'!=. -| ^▷. {→_.'} v; goal -| W. h;
prop/thm →.. ◀ W.
prf →.. // W.'!=. -| pr:0 p; →.. -| W. h;
!prop/thm →..' ◀ W.
prf →..' / →.. / ⊂. / ^▷. -| pr:0 ,, ap. p; →..' -| W. h;
thm `∅ → X = \{ set ∅ \}` ◀ W.
prf goal /// W.'!=. -| O p; goal -| W. h;
thm `X {/}= ∅ ⟹ X → ∅ = ∅` ◀ W.
prf goal /// W.'!=. -| O p; goal -| W. h;
prop/thm →∘ ◀ W.
prf →∘ / →.' / ∘. -| pr:0 p; →∘ -| W. h;

subsection 制限
word rest
prop rest.
prop/thm →rest ◀ W.
prf →rest // W.'!=. -| pr:0 p; →rest -| W. h;
br
!txt 次のwordってword+では？
word Rest
prop Rest.
prop/thm →_.𝕍 ◀ W.
prf →_.𝕍 / ⊂. -| pr:0 ,, ap. ,, ^◁!. p; →_.𝕍 -| W. h;
thm `[ f ; g col ∈_ X →_ 𝕍 ] ⟹ f = g ⇔ [ ∀ x ∈ X . f ap (x) = g ap (x) ]` ◀ W.

prf goal / →_.𝕍 -| =. v; goal -| W. h;

subsection 一点集合と写像
thm `\{ set x \} → Y =_ \{ \{ set \< pr x ; y \> \} Cls y | y ∈ Y \}` ◀ W.
prf goal // W.'!=. -| pr:0 p; goal -| W. h;
!txt 次のthmは削除して。特にBookに書く意味はないと思う。
thm `X ^^pr Y =_ ⋃_ [ \{ set \< pr x ; y \> \} -Cls x ; y | x ∈ X and y ∈ Y ]` ◀ W.
prf goal / ^^pr. -| set1. p; goal -| W. h;
br
word on
prop on.
thm `y on _ X = X ^^pr \{ set y \}` ◀ W.
prf goal / =. // W.'!=. -| O p; goal -| W. h;
thm `X → \{ set y \} = \{ set y on _ X \}` ◀ W.
prf goal / set1.' / →. /22 =. / set1. / on. -| pr:0 {→_.'} p; goal -| W. h;

subsection 写像の和
prop/thm →cup ◀ W.
prf LA1 <- `f1 ∈_ X1 →_ 𝕍 ⟹ ( x ∈ X1 ⇒ \< pr x ; f1 ap (x) \> ∈ f1 ∪ f2 )` / ∪. -| ap. ,, ^◁!. ,, ⊂. p;
    LA2 <- `( f1 ∈_ X1 →_ 𝕍 and f2 ∈_ X2 →_ 𝕍 and [ ∀ x ∈ X1 ∩ X2 . f1 ap (x) = f2 ap (x) ] ) ⟹ ( x ∈ X1 ⇒ ( \< pr x ; y \> ∈ f1 ∪ f2 ⇒ y = f1 ap (x) ) )` / ∪. / ∩. -| ap. ,, ^◁!. ,, ⊂. ,, pr:0 p;
    LA3 <- `( f1 ∈_ X1 →_ 𝕍 and f2 ∈_ X2 →_ 𝕍 and [ ∀ x ∈ X1 ∩ X2 . f1 ap (x) = f2 ap (x) ] ) ⟹ ( x ∈ X1 ⇒ x ∈ ^◁! ( f1 ∪ f2 ) )` / ^◁!. -| LA1 ,, LA2 v;
    LA <- `( f1 ∈_ X1 →_ 𝕍 and f2 ∈_ X2 →_ 𝕍 and [ ∀ x ∈ X1 ∩ X2 . f1 ap (x) = f2 ap (x) ] ) ⟹ ( x ∈ X1 ⇒ ( f1 ∪ f2 ) ap (x) = f1 ap (x) )` -| LA1 ,, LA3 ,, ap. v;
    LB1 <- `f2 ∈_ X2 →_ 𝕍 ⟹ ( x ∈ X2 ⇒ \< pr x ; f2 ap (x) \> ∈ f1 ∪ f2 )` / ∪. -| ap. ,, ^◁!. ,, ⊂. p;
    LB2 <- `( f1 ∈_ X1 →_ 𝕍 and f2 ∈_ X2 →_ 𝕍 and [ ∀ x ∈ X1 ∩ X2 . f1 ap (x) = f2 ap (x) ] ) ⟹ ( x ∈ X2 ⇒ ( \< pr x ; y \> ∈ f1 ∪ f2 ⇒ y = f2 ap (x) ) )` / ∪. / ∩. -| ap. ,, ^◁!. ,, ⊂. ,, pr:0 p;
    LB3 <- `( f1 ∈_ X1 →_ 𝕍 and f2 ∈_ X2 →_ 𝕍 and [ ∀ x ∈ X1 ∩ X2 . f1 ap (x) = f2 ap (x) ] ) ⟹ ( x ∈ X2 ⇒ x ∈ ^◁! ( f1 ∪ f2 ) )` / ^◁!. -| LB1 ,, LB2 v;
    LB <- `( f1 ∈_ X1 →_ 𝕍 and f2 ∈_ X2 →_ 𝕍 and [ ∀ x ∈ X1 ∩ X2 . f1 ap (x) = f2 ap (x) ] ) ⟹ ( x ∈ X2 ⇒ ( f1 ∪ f2 ) ap (x) = f2 ap (x) )` -| LB1 ,, LB3 ,, ap. v;
    C1 <- `( f1 ∈_ X1 →_ 𝕍 and f2 ∈_ X2 →_ 𝕍 and [ ∀ x ∈ X1 ∩ X2 . f1 ap (x) = f2 ap (x) ] ) ⟹ f1 ∪ f2 ⊂_ ( X1 ∪ X2 ) ^^pr_ 𝕍` -| ∪. p;
    CU <- `[ ∀ x ∈ X1 . x ∈ Z ] and [ ∀ x ∈ X2 . x ∈ Z ] ⟹ X1 ∪ X2 ⊂ Z` / ⊂. / ∪. -| O p;
    C2 <- `( f1 ∈_ X1 →_ 𝕍 and f2 ∈_ X2 →_ 𝕍 and [ ∀ x ∈ X1 ∩ X2 . f1 ap (x) = f2 ap (x) ] ) ⟹ X1 ∪ X2 ⊂ ^◁! ( f1 ∪ f2 )` -| CU ,, LA3 ,, LB3 {→_.-} p;
    CM <- `( f1 ∈_ X1 →_ 𝕍 and f2 ∈_ X2 →_ 𝕍 and [ ∀ x ∈ X1 ∩ X2 . f1 ap (x) = f2 ap (x) ] ) ⟹ f1 ∪ f2 ∈_ X1 ∪ X2 →_ 𝕍` -| C1 ,, C2 v;
    →cup -| CM ,, LA ,, LB {→_.-} p;
    →cup -| W. h;
!txt 上のprfは汚いね… このようなprfでは P^ := `f1 ∈_ X1 →_ 𝕍 and f2 ∈_ X2 →_ 𝕍 and [ ∀ x ∈ X1 ∩ X2 . f1 ap (x) = f2 ap (x)` と置くように。prfについては、定数化した方が速いのでは？ |f1 ∈_ |X1 →_ 𝕍 , |f2 ∈_ |X2 →_ 𝕍 , [ ∀ x ∈ |X1 ∩ |X2 . |f1 ap (x) = |f2 ap (x) ] をすべてsosに置ける。
prop/thm →cup2 ◀ W.
prf →cup2 / →..' / ∪. -| →cup {→_.-} v; →cup2 -| W. h;

subsection Knaster-Tarskiの不動点定理
let/thm KT <- `F ∈ ℘ X → ℘ X and [ ∀ A ; B \, ( [ chain A ⊂ B ⊂ X ] ⟹ F ap (A) ⊂ F ap (B) ) ] ⟹ [ ∃ A ∈ ℘ X . F ap (A) = A ]` ◀ W. ,, ax_s
prf K_ := `\{ cls B | B ⊂ X and F ap (B) ⊂ B \}` ; M_ := `[ ∀ A ; B \, ( [ chain A ⊂ B ⊂ X ] ⟹ F ap (A) ⊂ F ap (B) ) ]` ; LeCbd <- `K_ ⊂_ ℘ X` /// W. -| O p; LeE <- `Exi K_` -| LeCbd ,, ax_s[C_:=`K_`] p; LFX <- `F ∈ ℘ X → ℘ X and B ⊂ X ⟹ F ap (B) ⊂ X` -| →..' ,, ℘. p; LX <- `C =_ K_ and F ∈ ℘ X → ℘ X ⟹ X ∈ C` // W.!→. -| LFX ,, ⊂. p; LLow <- `C =_ K_ and F ∈ ℘ X → ℘ X and M_ and B ∈ C ⟹ F ap (⋂ C) ⊂ B` -| ⋂⊂ ,, ⊂. p; LPre <- `C =_ K_ and F ∈ ℘ X → ℘ X and M_ ⟹ F ap (⋂ C) ⊂ ⋂ C` -| LX ,, LLow ,, ⊂⋂ ,, ∅.' v; LIn <- `C =_ K_ and F ∈ ℘ X → ℘ X and M_ ⟹ F ap (⋂ C) ∈ C` // W.!→.!⊂. -| LPre ,, LX ,, ⋂⊂ ,, LFX v; LPost <- `C =_ K_ and F ∈ ℘ X → ℘ X and M_ ⟹ ⋂ C ⊂ F ap (⋂ C)` -| LIn ,, ⋂⊂ p; LFix <- `C =_ K_ and F ∈ ℘ X → ℘ X and M_ ⟹ ⋂ C ∈ ℘ X and F ap (⋂ C) = ⋂ C` / =. -| LPre ,, LPost ,, LX ,, ⋂⊂ ,, ℘. ,, ⊂. v; KT -| LFix ,, LeE p; KT -| W. ,, ax_s h;
!txt 上のprfで F を f に、C を K にして。LeE 行 も一行にして。

newpage
section 集合の大きさ比較

subsection 単射、全射、全単射
word →I →S →IS
prop →I.
!prop/thm →I.' ◀ W.
prf →I.' //// W.!=. -| sw. p; →I.' -| W. h;
prop →S.
!prop/thm →S.' ◀ W.
prf →S.' / →S. / →.. -| ^▷. ,, =. ,, ⊂. p; →S.' -| W. h;
!txt 上のprfは / W. を使ってもうちょっと綺麗にならない？
prop/thm →I.. ◀ W.
prf L <- `f ∈ X → Y ⟹ ( \< pr x ; y \> ∈ f ⟺ x ∈ X and y = f ap (x) )` // W.'!=. -| ap. ,, pr:0 p;
    →I.. / →I.' -| L p;
    →I.. -| W. h;
!txt Thm査読の結果画面で、このprfの OK を押すと　L <- の L がtexになってしまっている。そもそも L は要らないと思う。→.. {→_.𝕍} 辺りを使って
prop/thm →S.. ◀ W.
prf →S.. // W.'!=. -| pr:0 ,, ap. p; →S.. -| W. h;
prop/thm →S:0 ◀ W.
prf →S:0 / →S. -| O p; →S:0 -| W. h;
prop →IS.
!prop/thm →IS.' ◀ W.
prf →IS.' /// W.'!=. -| pr:0 p; →IS.' -| W. h;
prop/thm →IS^sw ◀ W.
prf →IS^sw /// W.'!=. -| sw. p; →IS^sw -| W. h;
br
prop/thm →I∘ ◀ W.
prf →I∘ / →I.' / ∘. -| →∘ ,, pr:0 p; →I∘ -| W. h;
prop/thm →S∘ ◀ W.
prf →S∘ / →S.' / ∘. -| →∘ ,, pr:0 ,, →.' p; →S∘ -| W. h;
prop/thm →IS∘ ◀ W.
prf →IS∘ / →IS. / ∩. -| →I∘ ,, →S∘ p; →IS∘ -| W. h;

subsection 恒等写像
word id
prop id.
prop/thm id:0 ◀ W.
prf id:0 /// W.'!=. -| pr:0 p; id:0 -| W. h;
prop/thm ∘E ◀ W.
prf ∘E / =. // W.!=. -| pr:0 p; ∘E -| W. h;
thm `R ∈_ Rel ⟹ R rest _ X = R ∘ id _ X` ◀ W.
prf goal / =. // W.!=. -| pr:0 p; goal -| W. h;
prop/thm →I... ◀ W.
prf L1 <- `f ∈ X →I Y ⟹ f ^sw ∘ f = id _ X` / =. // W.'!=. -| pr:0 ,, sw. p;
    L2 <- `f ∈ X → Y and g ∘ f = id _ X ⟹ f ∈ X →I Y` / =. // W.'!=. -| pr:0 p;
    →I... -| L1 ,, L2 ,, →I.' p;
    →I... -| W. h;
prop/thm →S... ◀ W.
prf L1 <- `f ∈ X →S Y ⟹ f ∘ f ^sw = id _ Y` / =. // W.'!=. -| pr:0 ,, sw. p;
    L2 <- `f ∈ X → Y and f ∘ g = id _ Y ⟹ f ∈ X →S Y` / =. // W.'!=. -| pr:0 p;
    →S... -| L1 ,, L2 ,, →S.' p;
    →S... -| W. h;
thm `X {/}= ∅ ⟹ X →I Y =_ \{ cls f ∈ X → Y | [ ∃ g ∈ Y → X . g ∘ f = id _ X ] \}` ◀ W.
prf G0 := `f ^sw ∪ ( ( Y ∖ ^▷ (f) ) ^^pr \{ set x0 \} )` ;
    Lmem <- `f ∈ X → Y ⟹ ( \< pr y ; x \> ∈ G0 ⟺ \< pr x ; y \> ∈ f or ( ( y ∈ Y and ¬ y ∈ ^▷ (f) ) and x = x0 ) )` / ∪. / ^sw. / ^^pr. / ∖. -| pr:0 ,, set1. ,, sw. ,, →.' p;
    Lsub <- `f ∈ X → Y and x0 ∈ X ⟹ G0 ⊂ Y ^^pr X` / ⊂. / ∪. / ^sw. / ^^pr. / ∖. -| pr:0 ,, set1. ,, sw. ,, →.' ,, ^^pr. v;
    Lex <- `f ∈ X → Y and x0 ∈ X and y ∈ Y ⟹ ∃ x \, \< pr y ; x \> ∈ G0` -| Lmem ,, ^▷. p;
    Lun <- `f ∈ X →I Y and \< pr y ; x1 \> ∈ G0 and \< pr y ; x2 \> ∈ G0 ⟹ x1 = x2` / →I.' -| Lmem ,, ^▷. p;
    LYX <- `f ∈ X →I Y and x0 ∈ X ⟹ G0 ∈ Y → X` / →.' -| Lsub ,, Lex ,, Lun ,, →I.' ,, ⊂. ,, ^^pr. ,, pr:0 p;
    Lcomp <- `f ∈ X →I Y ⟹ G0 ∘ f = id _ X` / =. / ∘. / id. -| Lmem ,, ^▷. ,, pr:0 ,, →I.' ,, →.' p;
    Lhard <- `f ∈ X →I Y and x0 ∈ X ⟹ [ ∃ g ∈ Y → X . g ∘ f = id _ X ]` -| LYX ,, Lcomp p;
    goal -| Lhard ,, →I... ,, →I.' ,, ∅.' p;
    goal -| W. h;

subsection 濃度
word =# ≤# <#
prop =#.
prop ≤#.
prop <#.
!prop/thm =#.' ◀ W.
prf =#.' / =#. / ∅.' -| O p; =#.' -| W. h;
!prop/thm ≤#.' ◀ W.
prf ≤#.' / ≤#. / ∅.' -| O p; ≤#.' -| W. h;
prop/thm =#:RTX ◀ W.
prf =#:RTX / =#.' -| id:0 ,, →IS∘ ,, →IS^sw p; =#:RTX -| W. h;
!prop/thm =#:X ◀ W.
prf =#:X / =#.' -| →IS^sw p; =#:X -| W. h;
prop/thm ≤#:RT ◀ W.
prf ≤#:RT / ≤#.' -| id:0 / →IS. / ∩. ,, →I∘ p; ≤#:RT -| W. h;
prop/thm sub_≤# ◀ W.
prf L <- `X ⊂ Y ⟹ id _ X ∈ X →I Y` /// W.'!=. -| pr:0 p; sub_≤# / ≤#.' -| L p; sub_≤# -| W. h;
prop/thm =#0 ◀ W.
prf =#0 //// W.'!=. -| O p; =#0 -| W. h;
!let/thm CSBpiece <- `f ∈ X →I Y and g ∈ Y →I X and A ⊂ X and A = (X ∖ ^▷ (g)) ∪ (g *^ap (f *^ap (A))) ⟹ X =# Y` ◀ W.
prf H_ := `((f ∩ (A ^^pr Y)) ∪ ((g ^sw) ∩ ((X ∖ A) ^^pr Y)))` ;
    Φ_ := `(X ∖ ^▷ (g)) ∪ (g *^ap (f *^ap (A)))` ;
    LeGval <- `g ∈ Y → X and \< pr y ; x \> ∈ g ⟹ x ∈ X` / →.' -| pr:0 p;
    LeUnL <- `P ⊂ P ∪ Q` -| ∪. ,, ⊂. p;
    LeUnR <- `Q ⊂ P ∪ Q` -| ∪. ,, ⊂. p;
    LeDif <- `u ∈ U ∖ B ⟹ u {/}∈ B` -| ∖. p;
    LeSubE <- `A ⊂ X and x ∈ A ⟹ x ∈ X` -| ⊂. p;
    LeGdom <- `g ∈ Y → X and \< pr y ; x \> ∈ g ⟹ y ∈ Y` / →.' -| pr:0 p;
    LeTmem <- `A ⊂ X and g ∈ Y → X ⟹ [ ∀ u ; v (\< pr u ; v \> ∈ H_ ⇔ (u ∈ X and v ∈ Y and ((u ∈ A and \< pr u ; v \> ∈ f) or (u ∈ X ∖ A and \< pr v ; u \> ∈ g)))) ]` / ∪. / ∩. / ^^pr. / ^sw. / ∖. / ⊂. -| pr:0 ,, sw. ,, →.' p;
    LeTsub <- `A ⊂ X ⟹ H_ ⊂ X ^^pr Y` / ⊂. / ∪. / ∩. / ^^pr. / ∖. -| O p;
    LeHcase <- `H = H_ and A ⊂ X and g ∈ Y → X and \< pr x ; y \> ∈ H ⟹ ((x ∈ A and \< pr x ; y \> ∈ f) or (x ∈ X ∖ A and y ∈ Y and \< pr y ; x \> ∈ g))` -| LeTmem p;
    LeHinA <- `H = H_ and A ⊂ X and g ∈ Y → X and x ∈ X and y ∈ Y and x ∈ A and \< pr x ; y \> ∈ f ⟹ \< pr x ; y \> ∈ H` -| LeTmem p;
    LeHinB <- `H = H_ and A ⊂ X and g ∈ Y → X and x ∈ X ∖ A and y ∈ Y and \< pr y ; x \> ∈ g ⟹ \< pr x ; y \> ∈ H` -| LeTmem ,, ∖. p;
    Lclosed <- `A = Φ_ ⟹ (g *^ap (f *^ap (A))) ⊂ A` -| LeUnR p;
    Loutside <- `g ∈ Y → X and A = Φ_ ⟹ [ ∀ x ∈ X ∖ A . [ ∃ y ∈ Y . \< pr y ; x \> ∈ g ] ]` -| LeUnL ,, ⊂. ,, ^▷. ,, LeGdom ,, ∖. p;
    LsepBase <- `F ∈ U →I V and G ∈ V →I U and [ ∀ z (z ∈ G *^ap (F *^ap (B)) ⟹ z ∈ B) ] and x ∈ U ∖ B and y ∈ V and \< pr y ; x \> ∈ G ⟹ y {/}∈ F *^ap (B)` -| *^ap. ,, LeDif p;
    Lsep <- `f ∈ X →I Y and g ∈ Y →I X and A = Φ_ and x ∈ X ∖ A and y ∈ Y and \< pr y ; x \> ∈ g ⟹ y {/}∈ f *^ap (A)` -| Lclosed ,, ⊂. ,, LsepBase p;
    Lftot <- `f ∈ X → Y ⟹ [ ∀ x ∈ X . [ ∃ y \, \< pr x ; y \> ∈ f ] ]` / →.' -| O p;
    LmA <- `H = H_ and f ∈ X → Y and g ∈ Y → X and A ⊂ X and x ∈ A ⟹ [ ∃ y \, \< pr x ; y \> ∈ H ]` -| Lftot ,, LeGval ,, LeHinA ,, LeSubE p;
    LmB <- `H = H_ and g ∈ Y → X and A ⊂ X and A = Φ_ and x ∈ X ∖ A ⟹ [ ∃ y \, \< pr x ; y \> ∈ H ]` -| Loutside ,, LeHinB p;
    LmapTot <- `H = H_ and f ∈ X → Y and g ∈ Y → X and A ⊂ X and A = Φ_ ⟹ [ ∀ x ∈ X . [ ∃ y \, \< pr x ; y \> ∈ H ] ]` -| LmA ,, LmB ,, ∖. p;
    Lfuniq <- `f ∈ X → Y and x ∈ X and \< pr x ; y0 \> ∈ f and \< pr x ; y1 \> ∈ f ⟹ y0 = y1` / →.' -| O p;
    LmapUniq <- `H = H_ and f ∈ X → Y and g ∈ Y →I X and A ⊂ X ⟹ [ ∀ x ; y0 ; y1 (\< pr x ; y0 \> ∈ H and \< pr x ; y1 \> ∈ H ⟹ y0 = y1) ]` -| LeHcase ,, Lfuniq ,, LeDif ,, LeSubE ,, →I.' p;
    LinjAB <- `f ∈ X →I Y and g ∈ Y →I X and A = Φ_ and x0 ∈ A and \< pr x0 ; y \> ∈ f and x1 ∈ X ∖ A and y ∈ Y and \< pr y ; x1 \> ∈ g ⟹ ⊥` -| Lsep ,, *^ap. p;
    LiA <- `H = H_ and f ∈ X →I Y and g ∈ Y →I X and g ∈ Y → X and A ⊂ X and A = Φ_ and x0 ∈ A and \< pr x0 ; y \> ∈ f and \< pr x1 ; y \> ∈ H ⟹ x0 = x1` -| LeHcase ,, →I.' ,, LinjAB p;
    LiB <- `H = H_ and f ∈ X →I Y and g ∈ Y →I X and g ∈ Y → X and A ⊂ X and A = Φ_ and x0 ∈ X ∖ A and y ∈ Y and \< pr y ; x0 \> ∈ g and \< pr x1 ; y \> ∈ H ⟹ x0 = x1` -| LeHcase ,, Lfuniq ,, LinjAB p;
    LinjPt <- `H = H_ and f ∈ X →I Y and g ∈ Y →I X and g ∈ Y → X and A ⊂ X and A = Φ_ ⟹ [ ∀ x0 ; x1 ; y (\< pr x0 ; y \> ∈ H and \< pr x1 ; y \> ∈ H ⟹ x0 = x1) ]` -| LeHcase ,, LiA ,, LiB p;
    LinA <- `A = Φ_ and x ∈ A and x ∈ ^▷ (g) ⟹ x ∈ (g *^ap (f *^ap (A)))` -| ∪. ,, ∖. p;
    Lback <- `g ∈ Y → X and g ∈ Y →I X and A = Φ_ ⟹ [ ∀ y ∈ Y ∖ (f *^ap (A)) . [ ∃ x ∈ X ∖ A . \< pr y ; x \> ∈ g ] ]` / ∖. -| Lftot ,, LeGval ,, →I.' ,, LinA ,, ^▷. ,, *^ap. p;
    Lsurj0 <- `g ∈ Y → X and g ∈ Y →I X and A ⊂ X and A = Φ_ ⟹ [ ∀ y ∈ Y . ([ ∃ x \, (x ∈ X and x ∈ A and \< pr x ; y \> ∈ f) ] or [ ∃ x \, (x ∈ X ∖ A and \< pr y ; x \> ∈ g) ]) ]` -| Lback ,, *^ap. ,, ∖. ,, LeSubE p;
    LsurjPt <- `H = H_ and g ∈ Y → X and g ∈ Y →I X and A ⊂ X and A = Φ_ ⟹ [ ∀ y ∈ Y . [ ∃ x \, \< pr x ; y \> ∈ H ] ]` -| Lsurj0 ,, LeHinA ,, LeHinB p;
    Lmap <- `f ∈ X →I Y and g ∈ Y →I X and A ⊂ X and A = Φ_ and H = H_ ⟹ H ∈ X → Y` / →.' -| LmapTot ,, LmapUniq ,, LeTsub ,, →I.' ,, ⊂. ,, ^^pr. p;
    Lpiece_c <- `f ∈ X →I Y and g ∈ Y →I X and A ⊂ X and A = Φ_ and H = H_ ⟹ H ∈ X →IS Y` / →IS. / ∩. -| Lmap ,, LinjPt ,, →I.' ,, →S.' ,, LsurjPt p;
    CSBpiece / =#.' -| Lpiece_c p;
    CSBpiece -| W. h;
let/thm CSB <- `[ chain X ≤# Y ≤# X ] ⟹ X =# Y` ◀ W. ,, ax_s
prf K_ := `\{ cls B | B ⊂ X and (X ∖ ^▷ (g)) ⊂ B and (g *^ap (f *^ap (B))) ⊂ B \}` ;
    Φ_ := `(X ∖ ^▷ (g)) ∪ (g *^ap (f *^ap (A)))` ;
    Φ0_ := `(X ∖ ^▷ (g)) ∪ (g *^ap (f *^ap (⋂ C)))` ;
    K^ := `[ ∀ B (B ∈ C ⇔ (B ⊂ X and (X ∖ ^▷ (g)) ⊂ B and (g *^ap (f *^ap (B))) ⊂ B)) ]` ;
    LeCbd <- `K_ ⊂_ ℘ X` /// W. -| pr:0 p;
    LeEC <- `Exi K_` -| LeCbd ,, ax_s[C_:=`K_`] p;
    LeGval <- `g ∈ Y → X and \< pr y ; x \> ∈ g ⟹ x ∈ X` / →.' -| pr:0 p;
    LeImX <- `g ∈ Y → X ⟹ g *^ap (Z) ⊂ X` -| *^ap. ,, ⊂. ,, LeGval p;
    LeX <- `f ∈ X → Y and g ∈ Y → X and K^ ⟹ X ∈ C` -| LeImX ,, ⊂. ,, ∖. p;
    LeNon <- `X ∈ C ⟹ C {/}= ∅` / ∅.' -| O p;
    Lmono <- `[ chain A ⊂ B ⊂ X ] and f ∈ X → Y and g ∈ Y → X ⟹ (g *^ap (f *^ap (A))) ⊂ (g *^ap (f *^ap (B)))` ///// W. -| pr:0 p;
    LeTrans <- `[ chain P ⊂ Q ⊂ R ] ⟹ P ⊂ R` -| ⊂. p;
    LeUnSub <- `P ⊂ B and Q ⊂ B ⟹ P ∪ Q ⊂ B` -| ∪. ,, ⊂. p;
    LeUnL <- `P ⊂ P ∪ Q` -| ∪. ,, ⊂. p;
    LeUnR <- `Q ⊂ P ∪ Q` -| ∪. ,, ⊂. p;
    LeDsubB <- `f ∈ X → Y and g ∈ Y → X and K^ and B ∈ C ⟹ Φ0_ ⊂ B` -| Lmono ,, ⋂⊂ ,, LeTrans ,, LeUnSub p;
    LeD1 <- `f ∈ X → Y and g ∈ Y → X and K^ ⟹ Φ0_ ⊂ ⋂ C` -| ⊂⋂ ,, LeDsubB ,, LeNon ,, LeX p;
    LeDX <- `g ∈ Y → X ⟹ Φ0_ ⊂ X` -| LeImX ,, ⊂. ,, ∪. ,, ∖. p;
    LeDc1 <- `f ∈ X → Y and g ∈ Y → X and K^ ⟹ (g *^ap (f *^ap (Φ0_))) ⊂ (g *^ap (f *^ap (⋂ C)))` -| Lmono ,, LeD1 ,, ⋂⊂ ,, LeX p;
    LeDclosed <- `f ∈ X → Y and g ∈ Y → X and K^ ⟹ (g *^ap (f *^ap (Φ0_))) ⊂ (Φ0_)` -| LeDc1 ,, LeTrans ,, LeUnR p;
    LeDin <- `f ∈ X → Y and g ∈ Y → X and K^ ⟹ Φ0_ ∈ C` -| LeDX ,, LeDclosed ,, LeUnL p;
    LeD2 <- `f ∈ X → Y and g ∈ Y → X and K^ ⟹ ⋂ C ⊂ Φ0_` -| ⋂⊂ ,, LeDin p;
    Lfix <- `f ∈ X → Y and g ∈ Y → X and K^ ⟹ ⋂ C = Φ0_` / =.. -| LeD1 ,, LeD2 p;
    Lfixed_c <- `f ∈ X → Y and g ∈ Y → X and K^ ⟹ [ ∃ A (A ⊂ X and A = Φ_) ]` -| ⋂⊂ ,, LeX ,, Lfix p;
    LeFamE <- `[ ∃ C \, K^ ]` -| LeEC p;
    Lfixed <- `f ∈ X →I Y and g ∈ Y →I X ⟹ [ ∃ A (A ⊂ X and A = Φ_) ]` / →I.' -| Lfixed_c ,, LeFamE p;
    CSB / ≤#.' -| Lfixed ,, CSBpiece p;
    CSB -| W. ,, ax_s h;
txt 単調写像の不動点（KT）を使っても示せます。
thm CSB ◀ W. ,, ax_s
prf Φ_ := `(X ∖ ^▷ (g)) ∪ (g *^ap (f *^ap (A)))` ;
    Φ1_ := `(X ∖ ^▷ (g)) ∪ (g *^ap (f *^ap (B)))` ;
    LeGval <- `g ∈ Y → X and \< pr y ; x \> ∈ g ⟹ x ∈ X` / →.' -| pr:0 p;
    LeImX <- `g ∈ Y → X ⟹ g *^ap (Z) ⊂ X` -| *^ap. ,, ⊂. ,, LeGval p;
    Lmono <- `[ chain A ⊂ B ⊂ X ] and f ∈ X → Y and g ∈ Y → X ⟹ (g *^ap (f *^ap (A))) ⊂ (g *^ap (f *^ap (B)))` ///// W. -| pr:0 p;
    LeTrans <- `[ chain P ⊂ Q ⊂ R ] ⟹ P ⊂ R` -| ⊂. p;
    F_ := `\{ \< pr B ; (X ∖ ^▷ (g)) ∪ (g *^ap (f *^ap (B))) \> Cls B | B ∈ ℘ X \}` ;
    LDX <- `g ∈ Y → X ⟹ Φ1_ ⊂ X` -| LeImX ,, ⊂. ,, ∪. ,, ∖. p;
    LeFs <- `g ∈ Y → X ⟹ F_ ⊂_ ℘ X ^^pr ℘ X` // W.!→.!⊂. -| LDX p;
    LeEF <- `g ∈ Y → X ⟹ Exi F_` -| LeFs ,, ax_s[C_:=`F_`] v;
    LDC <- `g ∈ Y → X ⟹ [ ∀ B ( B ⊂ X ⟹ Φ1_ ⊂ X ) ]` -| LDX p;
    LFsub <- `F =_ F_ and [ ∀ B ( B ⊂ X ⟹ Φ1_ ⊂ X ) ] and p ∈ F ⟹ [ ∃ x ∈ ℘ X . [ ∃ y ∈ ℘ X . p = \< pr x ; y \> ] ]` // W.!⊂. -| O p;
    LFtot <- `F =_ F_ and B ∈ ℘ X ⟹ \< pr B ; Φ1_ \> ∈ F` // W.!⊂. -| O p;
    LFfun <- `F =_ F_ and \< pr B ; P \> ∈ F and \< pr B ; Q \> ∈ F ⟹ P = Q` // W.!⊂.!=. -| pr:0 p;
    LFmap <- `F =_ F_ and [ ∀ B ( B ⊂ X ⟹ Φ1_ ⊂ X ) ] ⟹ F ∈ ℘ X → ℘ X` / →.' -| LFsub ,, LFtot ,, LFfun v;
    LFap <- `F =_ F_ and g ∈ Y → X and B ⊂ X ⟹ F ap (B) = Φ1_` -| LFmap ,, ap. ,, ^◁!. ,, ℘. ,, pr:0 p;
    LDmono <- `[ chain A ⊂ B ⊂ X ] and f ∈ X → Y and g ∈ Y → X ⟹ Φ_ ⊂ Φ1_` -| Lmono ,, ⊂. ,, ∪. v;
    LFmono <- `F =_ F_ and f ∈ X → Y and g ∈ Y → X ⟹ [ ∀ A ; B \, ( [ chain A ⊂ B ⊂ X ] ⟹ F ap (A) ⊂ F ap (B) ) ]` -| LFap ,, LDmono ,, LeTrans v;
    LfixF <- `F =_ F_ and f ∈ X → Y and g ∈ Y → X ⟹ [ ∃ A (A ⊂ X and A = Φ_) ]` -| KT ,, LFmap ,, LFmono ,, LFap ,, LDC ,, ℘. v;
    Lfixed <- `f ∈ X →I Y and g ∈ Y →I X ⟹ [ ∃ A (A ⊂ X and A = Φ_) ]` / →I.' -| LfixF ,, LeEF v;
    CSB / ≤#.' -| Lfixed ,, CSBpiece p;
    CSB -| W. ,, ax_s h;
!let/thm le_wp <- `X ≤# ℘ X` ◀ W. ,, ax_s
prf α_ := `\{ \< pr x ; \{ set x \} \> Cls x | x ∈ X \}` ;
    Leα <- `α_ ⊂_ X ^^pr ℘ X` // W.'!=. -| set1. p;
    LeI <- `α =_ α_ ⟹ α ∈ X →I ℘ X` /// W.'!=. -| pr:0 ,, set1. p;
    LeE <- `Exi α_` -| Leα ,, ax_s[C_:=`α_`] v;
    le_wp / ≤#.' -| LeI ,, LeE v;
    le_wp -| W. ,, ax_s h;
!let/thm cantor <- `X →S ℘ X = ∅` ◀ W. ,, ax_s
prf A_ := `\{ cls x ∈ X | {/}∃ y \, (\< pr x ; y \> ∈ f and x ∈ y) \}` ;
    LeA0 <- `A_ ⊂_ X` / W. -| O p;
    LeA <- `A =_ A_ and f ∈ X → ℘ X ⟹ A ∈ ℘ X and A {/}∈ ^▷ (f)` // W.'!=. -| pr:0 p;
    LeEA <- `Exi A_` -| LeA0 ,, ax_s[C_:=`A_`] p;
    LeS <- `A =_ A_ ⟹ ¬ f ∈ X →S ℘ X` / →S.' -| LeA / ^▷. p;
    Lno <- `¬ f ∈ X →S ℘ X` -| LeS ,, LeEA p;
    cantor / ∅.' -| Lno p;
    cantor -| W. ,, ax_s h;
thm `X <# ℘ X` ◀ W. ,, ax_s
prf goal / <#. [&l -| le_wp || &r / =#.' / →IS. / ∩. -| cantor ,, ∅.'] p;
    goal -| W. ,, ax_s h;

subsection 選択公理
word choice
prop choice.
!prop/thm choice.' ◀ W.
prf choice.' // W.'!=. -| pr:0 ,, ap. ,, ^◁!. p; choice.' -| W. h;
thm `X = \{ set x \} ⟹ choice (\{ set X \}) = \{ set \{ set \< pr X ; x \> \} \}` ◀ W.
prf L1 <- `X = \{ set x \} ⟹ \{ set \< pr X ; x \> \} ∈ choice (\{ set X \})` / choice.' / →.' / ⋃. -| pr:0 ,, set1. p;
    L2 <- `X = \{ set x \} and f ∈ choice (\{ set X \}) ⟹ f = \{ set \< pr X ; x \> \}` // W.'!=. -| set1. p;
    goal /2 set1.' -| L1 ,, L2 p;
    goal -| W. h;
thm `∅ ∈ calX ⟹ choice (calX) = ∅` ◀ W.
prf goal /// W.'!=. -| ∅. p; goal -| W. h;
prop ax_c
let/thm ACRI <- `@ax_c ⟺ [ ∀ X ; Y \, ( X →S Y =_ \{ cls f ∈ X → Y | [ ∃ g ∈ Y → X . f ∘ g = id _ Y ] \} ) ]` ◀ W. ,, ax_s
prf A5a1 <- `f ∈ X → Y ⟹ ( \< pr y ; x \> ∈ f ^sw ⟺ \< pr x ; y \> ∈ f )` / ^sw. -| sw. ,, →.' ,, pr:0 p;
    A5a4 <- `f ∈ X → Y and m ∈ f ^sw ∩ ( \{ set y \} ^^pr X ) ⟹ [ ∃ x ∈ X . m = \< pr y ; x \> and \< pr x ; y \> ∈ f ]` / ∩. / ^^pr. -| A5a1 ,, set1. ,, pr:0 v;
    A5a2 <- `c ∈ choice (F) and \< pr M ; m \> ∈ c ⟹ [ chain m ∈ M ∈ F ]` / choice.' / →.' -| pr:0 p;
    A3a <- `f ∈ X → Y and \< pr x ; y \> ∈ f ⟹ \< pr y ; x \> ∈ f ^sw ∩ ( \{ set y \} ^^pr X )` / ∩. / ^^pr. -| A5a1 ,, set1. ,, pr:0 ,, →.' v;
    A6a <- `c ∈ choice (F) and M ∈ F ⟹ ∃ m \, \< pr M ; m \> ∈ c` / choice.' / →.' -| pr:0 p;
    A7c <- `\< pr y ; x \> ∈ f ^sw ∩ ( \{ set y1 \} ^^pr X ) ⟹ y = y1` / ∩. / ^^pr. -| set1. ,, pr:0 p;
    A7b <- `c ∈ choice (F) and \< pr M ; m1 \> ∈ c and \< pr M ; m2 \> ∈ c ⟹ m1 = m2` / choice.' / →.' -| pr:0 p;
    A9a1 <- `p ∈ id _ Y ⟺ [ ∃ y ∈ Y . p = \< pr y ; y \> ]` /// W.'!=. -| pr:0 p;
    B0 <- `f ∈ X → Y and g ∈ Y → X and f ∘ g = id _ Y ⟹ f ∈ X →S Y` / =. // W.'!=. -| pr:0 p;
    Sto <- `f ∈ X →S Y ⟹ f ∈ X → Y` / →S.' -| O p;
    Ffun2 <- `f ∈ X → Y and \< pr x ; y \> ∈ f and \< pr x ; z \> ∈ f ⟹ y = z` / →.' -| pr:0 p;
    G9w1 <- `f ∈ X → Y and [ ∀ m ∈ g . [ ∃ y ∈ Y . [ ∃ x ∈ X . m = \< pr y ; x \> and \< pr x ; y \> ∈ f ] ] ] and [ ∀ y ∈ Y . ∃ x \, \< pr y ; x \> ∈ g ] ⟹ f ∘ g = id _ Y` /2 =. / ∘. -| A9a1 ,, Ffun2 ,, pr:0 v;
    A1a <- `y ∈ Y ⟹ f ^sw ∩ ( \{ set y \} ^^pr X ) ⊂ Y ^^pr X` / ⊂. / ∩. / ^^pr. -| set1. ,, pr:0 p;
    A1c <- `\{ cls M | [ ∃ y ∈ Y . M = f ^sw ∩ ( \{ set y \} ^^pr X ) ] \} ⊂_ ℘ ( Y ^^pr X )` -| A1a ,, ℘. v;
    A2 <- `Exi \{ cls M | [ ∃ y ∈ Y . M = f ^sw ∩ ( \{ set y \} ^^pr X ) ] \}` -| A1c ,, ax_s[C_:=`\{ cls M | [ ∃ y ∈ Y . M = f ^sw ∩ ( \{ set y \} ^^pr X ) ] \}`] v;
    HF <- `F =_ \{ cls M | [ ∃ y ∈ Y . M = f ^sw ∩ ( \{ set y \} ^^pr X ) ] \} ⟹ [ ∀ M ∈ F . [ ∃ y ∈ Y . M = f ^sw ∩ ( \{ set y \} ^^pr X ) ] ] and [ ∀ y ∈ Y . f ^sw ∩ ( \{ set y \} ^^pr X ) ∈ F ]` -| O p;
    A2p <- `∃ F \, ( [ ∀ M ∈ F . [ ∃ y ∈ Y . M = f ^sw ∩ ( \{ set y \} ^^pr X ) ] ] and [ ∀ y ∈ Y . f ^sw ∩ ( \{ set y \} ^^pr X ) ∈ F ] )` -| A2 ,, HF v;
    A3p <- `[ ∀ M ∈ F . [ ∃ y ∈ Y . M = f ^sw ∩ ( \{ set y \} ^^pr X ) ] ] and f ∈ X →S Y ⟹ ¬ ∅ ∈ F` / →S.' -| A3a ,, ∅.' v;
    A5c <- `[ ∀ M ∈ F . [ ∃ y ∈ Y . M = f ^sw ∩ ( \{ set y \} ^^pr X ) ] ] and c ∈ choice (F) and f ∈ X → Y ⟹ [ ∀ m ∈ ^▷ (c) . [ ∃ y ∈ Y . [ ∃ x ∈ X . m = \< pr y ; x \> and \< pr x ; y \> ∈ f ] ] ]` / ^▷. -| A5a2 ,, A5a4 v;
    A6c <- `[ ∀ y ∈ Y . f ^sw ∩ ( \{ set y \} ^^pr X ) ∈ F ] and c ∈ choice (F) and f ∈ X → Y ⟹ [ ∀ y ∈ Y . ∃ x \, \< pr y ; x \> ∈ ^▷ (c) ]` / ^▷. -| A6a ,, A5a2 ,, A5a4 v;
    A10f3 <- `[ ∀ M ∈ F . [ ∃ y ∈ Y . M = f ^sw ∩ ( \{ set y \} ^^pr X ) ] ] and [ ∀ y ∈ Y . f ^sw ∩ ( \{ set y \} ^^pr X ) ∈ F ] and c ∈ choice (F) and f ∈ X → Y ⟹ f ∘ ^▷ (c) = id _ Y` -| A5c ,, A6c ,, G9w1 v;
    A7d <- `[ ∀ M ∈ F . [ ∃ y ∈ Y . M = f ^sw ∩ ( \{ set y \} ^^pr X ) ] ] and c ∈ choice (F) and \< pr y ; x1 \> ∈ ^▷ (c) and \< pr y ; x2 \> ∈ ^▷ (c) ⟹ x1 = x2` / ^▷. -| A5a2 ,, A7c ,, A7b ,, pr:0 v;
    A8d <- `[ ∀ M ∈ F . [ ∃ y ∈ Y . M = f ^sw ∩ ( \{ set y \} ^^pr X ) ] ] and [ ∀ y ∈ Y . f ^sw ∩ ( \{ set y \} ^^pr X ) ∈ F ] and c ∈ choice (F) and f ∈ X → Y ⟹ ^▷ (c) ∈ Y → X` /2 →.' -| A5c ,, A6c ,, A7d v;
    A10g4 <- `[ ∀ M ∈ F . [ ∃ y ∈ Y . M = f ^sw ∩ ( \{ set y \} ^^pr X ) ] ] and [ ∀ y ∈ Y . f ^sw ∩ ( \{ set y \} ^^pr X ) ∈ F ] and c ∈ choice (F) and f ∈ X → Y ⟹ [ ∃ g ∈ Y → X . f ∘ g = id _ Y ]` -| A8d ,, A10f3 v;
    A10h4 <- `[ ∀ M ∈ F . [ ∃ y ∈ Y . M = f ^sw ∩ ( \{ set y \} ^^pr X ) ] ] and [ ∀ y ∈ Y . f ^sw ∩ ( \{ set y \} ^^pr X ) ∈ F ] and f ∈ X →S Y and choice (F) {/}= ∅ ⟹ [ ∃ g ∈ Y → X . f ∘ g = id _ Y ]` -| A10g4 ,, Sto ,, ∅.' v;
    A10u4 <- `[ ∀ calX {/}{-}∈ ∅ . choice (calX) {/}= ∅ ] and f ∈ X →S Y ⟹ [ ∃ g ∈ Y → X . f ∘ g = id _ Y ]` -| A2p ,, A3p ,, A10h4 v;
    D1 <- `[ ∀ calX {/}{-}∈ ∅ . choice (calX) {/}= ∅ ] ⟹ [ ∀ X ; Y \, ( X →S Y =_ \{ cls f ∈ X → Y | [ ∃ g ∈ Y → X . f ∘ g = id _ Y ] \} ) ]` -| A10u4 ,, B0 ,, Sto v;
    C1a <- `\{ cls p | [ ∃ A ∈ calX . [ ∃ a ∈ A . p = \< pr A ; a \> ] ] \} ⊂_ calX ^^pr ⋃ calX` /// W. -| pr:0 p;
    C1 <- `∃ R \, ( [ ∀ p ∈ R . [ ∃ A ∈ calX . [ ∃ a ∈ A . p = \< pr A ; a \> ] ] ] and [ ∀ A ∈ calX . [ ∀ a ∈ A . \< pr A ; a \> ∈ R ] ] )` -| C1a ,, ax_s[C_:=`\{ cls p | [ ∃ A ∈ calX . [ ∃ a ∈ A . p = \< pr A ; a \> ] ] \}`] v;
    C2a <- `\{ cls q | [ ∃ A ; a \, ( \< pr A ; a \> ∈ R and q = \< pr \< pr A ; a \> ; A \> ) ] \} ⊂_ R ^^pr ^◁ (R)` /// W. -| pr:0 p;
    C2 <- `∃ P \, ( [ ∀ q ∈ P . [ ∃ A ; a \, ( \< pr A ; a \> ∈ R and q = \< pr \< pr A ; a \> ; A \> ) ] ] and [ ∀ A ; a \, ( \< pr A ; a \> ∈ R ⇒ \< pr \< pr A ; a \> ; A \> ∈ P ) ] )` -| C2a ,, ax_s[C_:=`\{ cls q | [ ∃ A ; a \, ( \< pr A ; a \> ∈ R and q = \< pr \< pr A ; a \> ; A \> ) ] \}`] v;
    C3a <- `[ ∀ p ∈ R . [ ∃ A ∈ calX . [ ∃ a ∈ A . p = \< pr A ; a \> ] ] ] and [ ∀ q ∈ P . [ ∃ A ; a \, ( \< pr A ; a \> ∈ R and q = \< pr \< pr A ; a \> ; A \> ) ] ] ⟹ [ ∀ q ∈ P . [ ∃ p ∈ R . [ ∃ A ∈ calX . q = \< pr p ; A \> ] ] ]` -| pr:0 p;
    C3b <- `[ ∀ p ∈ R . [ ∃ A ∈ calX . [ ∃ a ∈ A . p = \< pr A ; a \> ] ] ] and [ ∀ A ; a \, ( \< pr A ; a \> ∈ R ⇒ \< pr \< pr A ; a \> ; A \> ∈ P ) ] ⟹ [ ∀ p ∈ R . ∃ A \, \< pr p ; A \> ∈ P ]` -| O p;
    C3c <- `[ ∀ q ∈ P . [ ∃ A ; a \, ( \< pr A ; a \> ∈ R and q = \< pr \< pr A ; a \> ; A \> ) ] ] and \< pr p ; B1 \> ∈ P and \< pr p ; B2 \> ∈ P ⟹ B1 = B2` -| pr:0 p;
    C3 <- `[ ∀ p ∈ R . [ ∃ A ∈ calX . [ ∃ a ∈ A . p = \< pr A ; a \> ] ] ] and [ ∀ q ∈ P . [ ∃ A ; a \, ( \< pr A ; a \> ∈ R and q = \< pr \< pr A ; a \> ; A \> ) ] ] and [ ∀ A ; a \, ( \< pr A ; a \> ∈ R ⇒ \< pr \< pr A ; a \> ; A \> ∈ P ) ] ⟹ P ∈ R → calX` / →.' -| C3a ,, C3b ,, C3c v;
    C4a <- `[ ∀ A ∈ calX . [ ∀ a ∈ A . \< pr A ; a \> ∈ R ] ] and [ ∀ A ; a \, ( \< pr A ; a \> ∈ R ⇒ \< pr \< pr A ; a \> ; A \> ∈ P ) ] and ¬ ∅ ∈ calX ⟹ [ ∀ A ∈ calX . ∃ p \, \< pr p ; A \> ∈ P ]` -| ∅.' p;
    C4 <- `[ ∀ p ∈ R . [ ∃ A ∈ calX . [ ∃ a ∈ A . p = \< pr A ; a \> ] ] ] and [ ∀ A ∈ calX . [ ∀ a ∈ A . \< pr A ; a \> ∈ R ] ] and [ ∀ q ∈ P . [ ∃ A ; a \, ( \< pr A ; a \> ∈ R and q = \< pr \< pr A ; a \> ; A \> ) ] ] and [ ∀ A ; a \, ( \< pr A ; a \> ∈ R ⇒ \< pr \< pr A ; a \> ; A \> ∈ P ) ] and ¬ ∅ ∈ calX ⟹ P ∈ R →S calX` / →S.' -| C3 ,, C4a v;
    C5 <- `[ ∀ X ; Y \, ( X →S Y =_ \{ cls f ∈ X → Y | [ ∃ g ∈ Y → X . f ∘ g = id _ Y ] \} ) ] and P ∈ R →S calX ⟹ [ ∃ g ∈ calX → R . P ∘ g = id _ calX ]` -| O p;
    C6z <- `P ∘ g = id _ calX and \< pr B ; p \> ∈ g and \< pr p ; A \> ∈ P ⟹ B = A` -| ∘. ,, A9a1 ,, pr:0 v;
    C6b <- `g ∈ calX → R and \< pr B ; p \> ∈ g ⟹ B ∈ calX and p ∈ R` / →.' -| pr:0 p;
    C6c <- `[ ∀ p ∈ R . [ ∃ A ∈ calX . [ ∃ a ∈ A . p = \< pr A ; a \> ] ] ] and [ ∀ A ; a \, ( \< pr A ; a \> ∈ R ⇒ \< pr \< pr A ; a \> ; A \> ∈ P ) ] and g ∈ calX → R and P ∘ g = id _ calX and \< pr B ; p \> ∈ g ⟹ [ ∃ a ∈ B . p = \< pr B ; a \> ]` -| C6b ,, C6z ,, pr:0 v;
    C7a <- `[ ∀ p ∈ R . [ ∃ A ∈ calX . [ ∃ a ∈ A . p = \< pr A ; a \> ] ] ] and [ ∀ A ; a \, ( \< pr A ; a \> ∈ R ⇒ \< pr \< pr A ; a \> ; A \> ∈ P ) ] and g ∈ calX → R and P ∘ g = id _ calX and m ∈ ^▷ (g) ⟹ [ ∃ B ∈ calX . [ ∃ a ∈ B . m = \< pr B ; a \> ] ]` / ^▷. -| C6b ,, C6c v;
    C7b1 <- `g ∈ calX → R and B ∈ calX ⟹ ∃ p \, \< pr B ; p \> ∈ g` / →.' -| O p;
    C7b <- `[ ∀ p ∈ R . [ ∃ A ∈ calX . [ ∃ a ∈ A . p = \< pr A ; a \> ] ] ] and [ ∀ A ; a \, ( \< pr A ; a \> ∈ R ⇒ \< pr \< pr A ; a \> ; A \> ∈ P ) ] and g ∈ calX → R and P ∘ g = id _ calX and B ∈ calX ⟹ ∃ a \, \< pr B ; a \> ∈ ^▷ (g)` / ^▷. -| C7b1 ,, C6c v;
    C7c1 <- `[ ∀ p ∈ R . [ ∃ A ∈ calX . [ ∃ a ∈ A . p = \< pr A ; a \> ] ] ] and [ ∀ A ; a \, ( \< pr A ; a \> ∈ R ⇒ \< pr \< pr A ; a \> ; A \> ∈ P ) ] and g ∈ calX → R and P ∘ g = id _ calX and \< pr x ; \< pr B ; a \> \> ∈ g ⟹ x = B` -| C6c ,, pr:0 v;
    C7cL2 <- `[ ∀ p ∈ R . [ ∃ A ∈ calX . [ ∃ a ∈ A . p = \< pr A ; a \> ] ] ] and [ ∀ A ; a \, ( \< pr A ; a \> ∈ R ⇒ \< pr \< pr A ; a \> ; A \> ∈ P ) ] and g ∈ calX → R and P ∘ g = id _ calX and \< pr B ; a1 \> ∈ ^▷ (g) and \< pr B ; a2 \> ∈ ^▷ (g) ⟹ \< pr B ; \< pr B ; a1 \> \> ∈ g and \< pr B ; \< pr B ; a2 \> \> ∈ g` / ^▷. -| C7c1 v;
    C7cM <- `g ∈ calX → R and \< pr B ; \< pr B ; a1 \> \> ∈ g and \< pr B ; \< pr B ; a2 \> \> ∈ g ⟹ a1 = a2` -| Ffun2 ,, pr:0 v;
    C7c <- `[ ∀ p ∈ R . [ ∃ A ∈ calX . [ ∃ a ∈ A . p = \< pr A ; a \> ] ] ] and [ ∀ A ; a \, ( \< pr A ; a \> ∈ R ⇒ \< pr \< pr A ; a \> ; A \> ∈ P ) ] and g ∈ calX → R and P ∘ g = id _ calX and \< pr B ; a1 \> ∈ ^▷ (g) and \< pr B ; a2 \> ∈ ^▷ (g) ⟹ a1 = a2` -| C7cL2 ,, C7cM v;
    C8a <- `[ ∀ p ∈ R . [ ∃ A ∈ calX . [ ∃ a ∈ A . p = \< pr A ; a \> ] ] ] and [ ∀ A ; a \, ( \< pr A ; a \> ∈ R ⇒ \< pr \< pr A ; a \> ; A \> ∈ P ) ] and g ∈ calX → R and P ∘ g = id _ calX ⟹ [ ∀ m ∈ ^▷ (g) . [ ∃ B ∈ calX . [ ∃ a ∈ ⋃ calX . m = \< pr B ; a \> ] ] ]` -| C7a ,, ⋃. v;
    C8 <- `[ ∀ p ∈ R . [ ∃ A ∈ calX . [ ∃ a ∈ A . p = \< pr A ; a \> ] ] ] and [ ∀ A ; a \, ( \< pr A ; a \> ∈ R ⇒ \< pr \< pr A ; a \> ; A \> ∈ P ) ] and g ∈ calX → R and P ∘ g = id _ calX ⟹ ^▷ (g) ∈ calX → ⋃ calX` /2 →.' -| C8a ,, C7b ,, C7c v;
    C9a <- `[ ∀ p ∈ R . [ ∃ A ∈ calX . [ ∃ a ∈ A . p = \< pr A ; a \> ] ] ] and [ ∀ A ; a \, ( \< pr A ; a \> ∈ R ⇒ \< pr \< pr A ; a \> ; A \> ∈ P ) ] and g ∈ calX → R and P ∘ g = id _ calX and \< pr X ; x \> ∈ ^▷ (g) ⟹ x ∈ X` / ^▷. -| C6b ,, C6c ,, pr:0 v;
    C9 <- `[ ∀ p ∈ R . [ ∃ A ∈ calX . [ ∃ a ∈ A . p = \< pr A ; a \> ] ] ] and [ ∀ A ; a \, ( \< pr A ; a \> ∈ R ⇒ \< pr \< pr A ; a \> ; A \> ∈ P ) ] and g ∈ calX → R and P ∘ g = id _ calX ⟹ ^▷ (g) ∈ choice (calX)` / choice.' -| C8 ,, C9a v;
    C10a <- `[ ∀ X ; Y \, ( X →S Y =_ \{ cls f ∈ X → Y | [ ∃ g ∈ Y → X . f ∘ g = id _ Y ] \} ) ] and [ ∀ p ∈ R . [ ∃ A ∈ calX . [ ∃ a ∈ A . p = \< pr A ; a \> ] ] ] and [ ∀ A ; a \, ( \< pr A ; a \> ∈ R ⇒ \< pr \< pr A ; a \> ; A \> ∈ P ) ] and P ∈ R →S calX ⟹ ∃ c \, c ∈ choice (calX)` -| C5 ,, C9 v;
    C10 <- `[ ∀ p ∈ R . [ ∃ A ∈ calX . [ ∃ a ∈ A . p = \< pr A ; a \> ] ] ] and [ ∀ A ∈ calX . [ ∀ a ∈ A . \< pr A ; a \> ∈ R ] ] and [ ∀ q ∈ P . [ ∃ A ; a \, ( \< pr A ; a \> ∈ R and q = \< pr \< pr A ; a \> ; A \> ) ] ] and [ ∀ A ; a \, ( \< pr A ; a \> ∈ R ⇒ \< pr \< pr A ; a \> ; A \> ∈ P ) ] and [ ∀ X ; Y \, ( X →S Y =_ \{ cls f ∈ X → Y | [ ∃ g ∈ Y → X . f ∘ g = id _ Y ] \} ) ] and ¬ ∅ ∈ calX ⟹ choice (calX) {/}= ∅` / ∅.' -| C4 ,, C10a v;
    D2 <- `[ ∀ X ; Y \, ( X →S Y =_ \{ cls f ∈ X → Y | [ ∃ g ∈ Y → X . f ∘ g = id _ Y ] \} ) ] ⟹ [ ∀ calX {/}{-}∈ ∅ . choice (calX) {/}= ∅ ]` -| C1 ,, C2 ,, C10 v;
    ACRI -| D1 ,, D2 v;
    ACRI -| W. ,, ax_s h;

subsection 直積
word ∏
prop ∏.
!prop/thm ∏.' ◀ W.
prf ∏.' -| ∏. v; ∏.' -| W. h;
thm `X ∈_ Λ →_ 𝕍 and ∅ ∈ ^▷ (X) ⟹ ∏ X = ∅` ◀ W.
prf L1 <- `X ∈_ Λ →_ 𝕍 and ∅ ∈ ^▷ (X) ⟹ [ ∃ λ ∈ Λ . X ap _ λ = ∅ ]` / ^▷. -| ap. ,, ⊂. ,, pr:0 v;
    L2 <- `X ∈_ Λ →_ 𝕍 and λ ∈ Λ and X ap _ λ = ∅ ⟹ x {/}∈ ∏ X` -| ∏. ,, ∅. v;
    goal -| L1 ,, L2 ,, =. ,, ∅. v;
    goal -| W. h;
prop Dp_c

standard_math/1-2.book

`standard_math/1-2.book`