Step | Hyp | Ref
| Expression |
1 | | cardon 9881 |
. . . . 5
β’
(cardβ(βͺ π΄ β π΅)) β On |
2 | 1 | onsuci 7775 |
. . . 4
β’ suc
(cardβ(βͺ π΄ β π΅)) β On |
3 | 2 | a1i 11 |
. . 3
β’ (π β suc (cardβ(βͺ π΄
β π΅)) β
On) |
4 | | onelon 6343 |
. . 3
β’ ((suc
(cardβ(βͺ π΄ β π΅)) β On β§ πΆ β suc (cardβ(βͺ π΄
β π΅))) β πΆ β On) |
5 | 3, 4 | sylan 581 |
. 2
β’ ((π β§ πΆ β suc (cardβ(βͺ π΄
β π΅))) β πΆ β On) |
6 | | eleq1 2826 |
. . . . . 6
β’ (π¦ = π β (π¦ β suc (cardβ(βͺ π΄
β π΅)) β π β suc (cardβ(βͺ π΄
β π΅)))) |
7 | | fveq2 6843 |
. . . . . . 7
β’ (π¦ = π β (πΊβπ¦) = (πΊβπ)) |
8 | 7 | eleq1d 2823 |
. . . . . 6
β’ (π¦ = π β ((πΊβπ¦) β π΄ β (πΊβπ) β π΄)) |
9 | 6, 8 | imbi12d 345 |
. . . . 5
β’ (π¦ = π β ((π¦ β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπ¦) β π΄) β (π β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπ) β π΄))) |
10 | 9 | imbi2d 341 |
. . . 4
β’ (π¦ = π β ((π β (π¦ β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπ¦) β π΄)) β (π β (π β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπ) β π΄)))) |
11 | | eleq1 2826 |
. . . . . 6
β’ (π¦ = πΆ β (π¦ β suc (cardβ(βͺ π΄
β π΅)) β πΆ β suc (cardβ(βͺ π΄
β π΅)))) |
12 | | fveq2 6843 |
. . . . . . 7
β’ (π¦ = πΆ β (πΊβπ¦) = (πΊβπΆ)) |
13 | 12 | eleq1d 2823 |
. . . . . 6
β’ (π¦ = πΆ β ((πΊβπ¦) β π΄ β (πΊβπΆ) β π΄)) |
14 | 11, 13 | imbi12d 345 |
. . . . 5
β’ (π¦ = πΆ β ((π¦ β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπ¦) β π΄) β (πΆ β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπΆ) β π΄))) |
15 | 14 | imbi2d 341 |
. . . 4
β’ (π¦ = πΆ β ((π β (π¦ β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπ¦) β π΄)) β (π β (πΆ β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπΆ) β π΄)))) |
16 | | r19.21v 3177 |
. . . . . 6
β’
(βπ β
π¦ (π β (π β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπ) β π΄)) β (π β βπ β π¦ (π β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπ) β π΄))) |
17 | 2 | onordi 6429 |
. . . . . . . . . . . . . . 15
β’ Ord suc
(cardβ(βͺ π΄ β π΅)) |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β Ord suc (cardβ(βͺ π΄
β π΅))) |
19 | | ordelss 6334 |
. . . . . . . . . . . . . 14
β’ ((Ord suc
(cardβ(βͺ π΄ β π΅)) β§ π¦ β suc (cardβ(βͺ π΄
β π΅))) β π¦ β suc (cardβ(βͺ π΄
β π΅))) |
20 | 18, 19 | sylan 581 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β suc (cardβ(βͺ π΄
β π΅))) β π¦ β suc (cardβ(βͺ π΄
β π΅))) |
21 | 20 | sselda 3945 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β suc (cardβ(βͺ π΄
β π΅))) β§ π β π¦) β π β suc (cardβ(βͺ π΄
β π΅))) |
22 | | biimt 361 |
. . . . . . . . . . . 12
β’ (π β suc (cardβ(βͺ π΄
β π΅)) β ((πΊβπ) β π΄ β (π β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπ) β π΄))) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β suc (cardβ(βͺ π΄
β π΅))) β§ π β π¦) β ((πΊβπ) β π΄ β (π β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπ) β π΄))) |
24 | 23 | ralbidva 3173 |
. . . . . . . . . 10
β’ ((π β§ π¦ β suc (cardβ(βͺ π΄
β π΅))) β
(βπ β π¦ (πΊβπ) β π΄ β βπ β π¦ (π β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπ) β π΄))) |
25 | 2 | onssi 7774 |
. . . . . . . . . . . . . 14
β’ suc
(cardβ(βͺ π΄ β π΅)) β On |
26 | | simprl 770 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β π¦ β suc (cardβ(βͺ π΄
β π΅))) |
27 | 25, 26 | sselid 3943 |
. . . . . . . . . . . . 13
β’ ((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β π¦ β On) |
28 | | ttukeylem.1 |
. . . . . . . . . . . . . 14
β’ (π β πΉ:(cardβ(βͺ
π΄ β π΅))β1-1-ontoβ(βͺ π΄ β π΅)) |
29 | | ttukeylem.2 |
. . . . . . . . . . . . . 14
β’ (π β π΅ β π΄) |
30 | | ttukeylem.3 |
. . . . . . . . . . . . . 14
β’ (π β βπ₯(π₯ β π΄ β (π« π₯ β© Fin) β π΄)) |
31 | | ttukeylem.4 |
. . . . . . . . . . . . . 14
β’ πΊ = recs((π§ β V β¦ if(dom π§ = βͺ dom π§, if(dom π§ = β
, π΅, βͺ ran π§), ((π§ββͺ dom π§) βͺ if(((π§ββͺ dom π§) βͺ {(πΉββͺ dom
π§)}) β π΄, {(πΉββͺ dom
π§)},
β
))))) |
32 | 28, 29, 30, 31 | ttukeylem3 10448 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β On) β (πΊβπ¦) = if(π¦ = βͺ π¦, if(π¦ = β
, π΅, βͺ (πΊ β π¦)), ((πΊββͺ π¦) βͺ if(((πΊββͺ π¦) βͺ {(πΉββͺ π¦)}) β π΄, {(πΉββͺ π¦)}, β
)))) |
33 | 27, 32 | syldan 592 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β (πΊβπ¦) = if(π¦ = βͺ π¦, if(π¦ = β
, π΅, βͺ (πΊ β π¦)), ((πΊββͺ π¦) βͺ if(((πΊββͺ π¦) βͺ {(πΉββͺ π¦)}) β π΄, {(πΉββͺ π¦)}, β
)))) |
34 | 29 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π¦ = β
) β π΅ β π΄) |
35 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β π€ β (π«
βͺ (πΊ β π¦) β© Fin)) |
36 | 35 | elin2d 4160 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β π€ β
Fin) |
37 | 35 | elin1d 4159 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β π€ β π«
βͺ (πΊ β π¦)) |
38 | 37 | elpwid 4570 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β π€ β βͺ (πΊ
β π¦)) |
39 | 31 | tfr1 8344 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ πΊ Fn On |
40 | | fnfun 6603 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (πΊ Fn On β Fun πΊ) |
41 | | funiunfv 7196 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (Fun
πΊ β βͺ π£ β π¦ (πΊβπ£) = βͺ (πΊ β π¦)) |
42 | 39, 40, 41 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ βͺ π£ β π¦ (πΊβπ£) = βͺ (πΊ β π¦) |
43 | 38, 42 | sseqtrrdi 3996 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β π€ β βͺ π£ β π¦ (πΊβπ£)) |
44 | | dfss3 3933 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π€ β βͺ π£ β π¦ (πΊβπ£) β βπ’ β π€ π’ β βͺ
π£ β π¦ (πΊβπ£)) |
45 | | eliun 4959 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π’ β βͺ π£ β π¦ (πΊβπ£) β βπ£ β π¦ π’ β (πΊβπ£)) |
46 | 45 | ralbii 3097 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(βπ’ β
π€ π’ β βͺ
π£ β π¦ (πΊβπ£) β βπ’ β π€ βπ£ β π¦ π’ β (πΊβπ£)) |
47 | 44, 46 | bitri 275 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ β βͺ π£ β π¦ (πΊβπ£) β βπ’ β π€ βπ£ β π¦ π’ β (πΊβπ£)) |
48 | 43, 47 | sylib 217 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β βπ’ β
π€ βπ£ β π¦ π’ β (πΊβπ£)) |
49 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π£ = (πβπ’) β (πΊβπ£) = (πΊβ(πβπ’))) |
50 | 49 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π£ = (πβπ’) β (π’ β (πΊβπ£) β π’ β (πΊβ(πβπ’)))) |
51 | 50 | ac6sfi 9232 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π€ β Fin β§ βπ’ β π€ βπ£ β π¦ π’ β (πΊβπ£)) β βπ(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’)))) |
52 | 36, 48, 51 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β βπ(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’)))) |
53 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π€ = β
β (π€ β π΄ β β
β π΄)) |
54 | | simp-4l 782 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β§ π€ β β
) β π) |
55 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = βͺ
ran π β (πΊβπ) = (πΊββͺ ran
π)) |
56 | 55 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = βͺ
ran π β ((πΊβπ) β π΄ β (πΊββͺ ran
π) β π΄)) |
57 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β βπ β π¦ (πΊβπ) β π΄) |
58 | 57 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β§ π€ β β
) β βπ β π¦ (πΊβπ) β π΄) |
59 | | simprrl 780 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β π:π€βΆπ¦) |
60 | 59 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β§ π€ β β
) β π:π€βΆπ¦) |
61 | | frn 6676 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π:π€βΆπ¦ β ran π β π¦) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β§ π€ β β
) β ran π β π¦) |
63 | 27 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β§ π€ β β
) β π¦ β On) |
64 | | onss 7720 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π¦ β On β π¦ β On) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β§ π€ β β
) β π¦ β On) |
66 | 62, 65 | sstrd 3955 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β§ π€ β β
) β ran π β On) |
67 | 36 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β π€ β Fin) |
68 | 67 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β§ π€ β β
) β π€ β Fin) |
69 | | ffn 6669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π:π€βΆπ¦ β π Fn π€) |
70 | 60, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β§ π€ β β
) β π Fn π€) |
71 | | dffn4 6763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π Fn π€ β π:π€βontoβran π) |
72 | 70, 71 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β§ π€ β β
) β π:π€βontoβran π) |
73 | | fofi 9283 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π€ β Fin β§ π:π€βontoβran π) β ran π β Fin) |
74 | 68, 72, 73 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β§ π€ β β
) β ran π β Fin) |
75 | | dm0rn0 5881 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (dom
π = β
β ran
π =
β
) |
76 | 59 | fdmd 6680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β dom π = π€) |
77 | 76 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β (dom π = β
β π€ = β
)) |
78 | 75, 77 | bitr3id 285 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β (ran π = β
β π€ = β
)) |
79 | 78 | necon3bid 2989 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β (ran π β β
β π€ β β
)) |
80 | 79 | biimpar 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β§ π€ β β
) β ran π β β
) |
81 | | ordunifi 9238 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((ran
π β On β§ ran
π β Fin β§ ran
π β β
) β
βͺ ran π β ran π) |
82 | 66, 74, 80, 81 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β§ π€ β β
) β βͺ ran π β ran π) |
83 | 62, 82 | sseldd 3946 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β§ π€ β β
) β βͺ ran π β π¦) |
84 | 56, 58, 83 | rspcdva 3583 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β§ π€ β β
) β (πΊββͺ ran
π) β π΄) |
85 | | simp-4l 782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β§ (π:π€βΆπ¦ β§ π’ β π€)) β π) |
86 | 27 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β§ (π:π€βΆπ¦ β§ π’ β π€)) β π¦ β On) |
87 | 86, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β§ (π:π€βΆπ¦ β§ π’ β π€)) β π¦ β On) |
88 | | ffvelcdm 7033 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π:π€βΆπ¦ β§ π’ β π€) β (πβπ’) β π¦) |
89 | 88 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β§ (π:π€βΆπ¦ β§ π’ β π€)) β (πβπ’) β π¦) |
90 | 87, 89 | sseldd 3946 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β§ (π:π€βΆπ¦ β§ π’ β π€)) β (πβπ’) β On) |
91 | 61 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β§ (π:π€βΆπ¦ β§ π’ β π€)) β ran π β π¦) |
92 | 91, 87 | sstrd 3955 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β§ (π:π€βΆπ¦ β§ π’ β π€)) β ran π β On) |
93 | | vex 3450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ π β V |
94 | 93 | rnex 7850 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ran π β V |
95 | 94 | ssonunii 7716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (ran
π β On β βͺ ran π β On) |
96 | 92, 95 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β§ (π:π€βΆπ¦ β§ π’ β π€)) β βͺ ran
π β
On) |
97 | 69 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β§ (π:π€βΆπ¦ β§ π’ β π€)) β π Fn π€) |
98 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β§ (π:π€βΆπ¦ β§ π’ β π€)) β π’ β π€) |
99 | | fnfvelrn 7032 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π Fn π€ β§ π’ β π€) β (πβπ’) β ran π) |
100 | 97, 98, 99 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β§ (π:π€βΆπ¦ β§ π’ β π€)) β (πβπ’) β ran π) |
101 | | elssuni 4899 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((πβπ’) β ran π β (πβπ’) β βͺ ran
π) |
102 | 100, 101 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β§ (π:π€βΆπ¦ β§ π’ β π€)) β (πβπ’) β βͺ ran
π) |
103 | 28, 29, 30, 31 | ttukeylem5 10450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ ((πβπ’) β On β§ βͺ ran π β On β§ (πβπ’) β βͺ ran
π)) β (πΊβ(πβπ’)) β (πΊββͺ ran
π)) |
104 | 85, 90, 96, 102, 103 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β§ (π:π€βΆπ¦ β§ π’ β π€)) β (πΊβ(πβπ’)) β (πΊββͺ ran
π)) |
105 | 104 | sseld 3944 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β§ (π:π€βΆπ¦ β§ π’ β π€)) β (π’ β (πΊβ(πβπ’)) β π’ β (πΊββͺ ran
π))) |
106 | 105 | anassrs 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β§ π:π€βΆπ¦) β§ π’ β π€) β (π’ β (πΊβ(πβπ’)) β π’ β (πΊββͺ ran
π))) |
107 | 106 | ralimdva 3165 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β§ π:π€βΆπ¦) β (βπ’ β π€ π’ β (πΊβ(πβπ’)) β βπ’ β π€ π’ β (πΊββͺ ran
π))) |
108 | 107 | expimpd 455 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β ((π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))) β βπ’ β π€ π’ β (πΊββͺ ran
π))) |
109 | 108 | impr 456 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β βπ’ β π€ π’ β (πΊββͺ ran
π)) |
110 | 109 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β§ π€ β β
) β βπ’ β π€ π’ β (πΊββͺ ran
π)) |
111 | | dfss3 3933 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π€ β (πΊββͺ ran
π) β βπ’ β π€ π’ β (πΊββͺ ran
π)) |
112 | 110, 111 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β§ π€ β β
) β π€ β (πΊββͺ ran
π)) |
113 | 28, 29, 30 | ttukeylem2 10447 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ ((πΊββͺ ran
π) β π΄ β§ π€ β (πΊββͺ ran
π))) β π€ β π΄) |
114 | 54, 84, 112, 113 | syl12anc 836 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β§ π€ β β
) β π€ β π΄) |
115 | | 0ss 4357 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ β
β π΅ |
116 | 28, 29, 30 | ttukeylem2 10447 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ (π΅ β π΄ β§ β
β π΅)) β β
β π΄) |
117 | 115, 116 | mpanr2 703 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β§ π΅ β π΄) β β
β π΄) |
118 | 29, 117 | mpdan 686 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β
β π΄) |
119 | 118 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β β
β π΄) |
120 | 53, 114, 119 | pm2.61ne 3031 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ (π€ β (π« βͺ (πΊ
β π¦) β© Fin) β§
(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))))) β π€ β π΄) |
121 | 120 | expr 458 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β ((π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))) β π€ β π΄)) |
122 | 121 | exlimdv 1937 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β (βπ(π:π€βΆπ¦ β§ βπ’ β π€ π’ β (πΊβ(πβπ’))) β π€ β π΄)) |
123 | 52, 122 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ π€ β (π« βͺ (πΊ
β π¦) β© Fin))
β π€ β π΄) |
124 | 123 | ex 414 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β (π€ β (π« βͺ (πΊ
β π¦) β© Fin)
β π€ β π΄)) |
125 | 124 | ssrdv 3951 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β (π« βͺ (πΊ
β π¦) β© Fin)
β π΄) |
126 | 28, 29, 30 | ttukeylem1 10446 |
. . . . . . . . . . . . . . . . 17
β’ (π β (βͺ (πΊ
β π¦) β π΄ β (π« βͺ (πΊ
β π¦) β© Fin)
β π΄)) |
127 | 126 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β (βͺ (πΊ
β π¦) β π΄ β (π« βͺ (πΊ
β π¦) β© Fin)
β π΄)) |
128 | 125, 127 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β βͺ (πΊ
β π¦) β π΄) |
129 | 128 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β§ Β¬ π¦ = β
) β βͺ (πΊ
β π¦) β π΄) |
130 | 34, 129 | ifclda 4522 |
. . . . . . . . . . . . 13
β’ (((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ π¦ = βͺ π¦) β if(π¦ = β
, π΅, βͺ (πΊ β π¦)) β π΄) |
131 | | uneq2 4118 |
. . . . . . . . . . . . . . 15
β’ ({(πΉββͺ π¦)}
= if(((πΊββͺ π¦)
βͺ {(πΉββͺ π¦)})
β π΄, {(πΉββͺ π¦)},
β
) β ((πΊββͺ π¦) βͺ {(πΉββͺ π¦)}) = ((πΊββͺ π¦) βͺ if(((πΊββͺ π¦) βͺ {(πΉββͺ π¦)}) β π΄, {(πΉββͺ π¦)}, β
))) |
132 | 131 | eleq1d 2823 |
. . . . . . . . . . . . . 14
β’ ({(πΉββͺ π¦)}
= if(((πΊββͺ π¦)
βͺ {(πΉββͺ π¦)})
β π΄, {(πΉββͺ π¦)},
β
) β (((πΊββͺ π¦) βͺ {(πΉββͺ π¦)}) β π΄ β ((πΊββͺ π¦) βͺ if(((πΊββͺ π¦) βͺ {(πΉββͺ π¦)}) β π΄, {(πΉββͺ π¦)}, β
)) β π΄)) |
133 | | un0 4351 |
. . . . . . . . . . . . . . . 16
β’ ((πΊββͺ π¦)
βͺ β
) = (πΊββͺ π¦) |
134 | | uneq2 4118 |
. . . . . . . . . . . . . . . 16
β’ (β
= if(((πΊββͺ π¦)
βͺ {(πΉββͺ π¦)})
β π΄, {(πΉββͺ π¦)},
β
) β ((πΊββͺ π¦) βͺ β
) = ((πΊββͺ π¦)
βͺ if(((πΊββͺ π¦)
βͺ {(πΉββͺ π¦)})
β π΄, {(πΉββͺ π¦)},
β
))) |
135 | 133, 134 | eqtr3id 2791 |
. . . . . . . . . . . . . . 15
β’ (β
= if(((πΊββͺ π¦)
βͺ {(πΉββͺ π¦)})
β π΄, {(πΉββͺ π¦)},
β
) β (πΊββͺ π¦) = ((πΊββͺ π¦) βͺ if(((πΊββͺ π¦) βͺ {(πΉββͺ π¦)}) β π΄, {(πΉββͺ π¦)}, β
))) |
136 | 135 | eleq1d 2823 |
. . . . . . . . . . . . . 14
β’ (β
= if(((πΊββͺ π¦)
βͺ {(πΉββͺ π¦)})
β π΄, {(πΉββͺ π¦)},
β
) β ((πΊββͺ π¦) β π΄ β ((πΊββͺ π¦) βͺ if(((πΊββͺ π¦) βͺ {(πΉββͺ π¦)}) β π΄, {(πΉββͺ π¦)}, β
)) β π΄)) |
137 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ Β¬ π¦ = βͺ π¦) β§ ((πΊββͺ π¦) βͺ {(πΉββͺ π¦)}) β π΄) β ((πΊββͺ π¦) βͺ {(πΉββͺ π¦)}) β π΄) |
138 | | fveq2 6843 |
. . . . . . . . . . . . . . . . 17
β’ (π = βͺ
π¦ β (πΊβπ) = (πΊββͺ π¦)) |
139 | 138 | eleq1d 2823 |
. . . . . . . . . . . . . . . 16
β’ (π = βͺ
π¦ β ((πΊβπ) β π΄ β (πΊββͺ π¦) β π΄)) |
140 | | simplrr 777 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ Β¬ π¦ = βͺ π¦) β βπ β π¦ (πΊβπ) β π΄) |
141 | | vuniex 7677 |
. . . . . . . . . . . . . . . . . 18
β’ βͺ π¦
β V |
142 | 141 | sucid 6400 |
. . . . . . . . . . . . . . . . 17
β’ βͺ π¦
β suc βͺ π¦ |
143 | | eloni 6328 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β On β Ord π¦) |
144 | | orduniorsuc 7766 |
. . . . . . . . . . . . . . . . . . 19
β’ (Ord
π¦ β (π¦ = βͺ
π¦ β¨ π¦ = suc βͺ π¦)) |
145 | 27, 143, 144 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β (π¦ = βͺ π¦ β¨ π¦ = suc βͺ π¦)) |
146 | 145 | orcanai 1002 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ Β¬ π¦ = βͺ π¦) β π¦ = suc βͺ π¦) |
147 | 142, 146 | eleqtrrid 2845 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ Β¬ π¦ = βͺ π¦) β βͺ π¦
β π¦) |
148 | 139, 140,
147 | rspcdva 3583 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ Β¬ π¦ = βͺ π¦) β (πΊββͺ π¦) β π΄) |
149 | 148 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ Β¬ π¦ = βͺ π¦) β§ Β¬ ((πΊββͺ π¦)
βͺ {(πΉββͺ π¦)})
β π΄) β (πΊββͺ π¦)
β π΄) |
150 | 132, 136,
137, 149 | ifbothda 4525 |
. . . . . . . . . . . . 13
β’ (((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β§ Β¬ π¦ = βͺ π¦) β ((πΊββͺ π¦) βͺ if(((πΊββͺ π¦) βͺ {(πΉββͺ π¦)}) β π΄, {(πΉββͺ π¦)}, β
)) β π΄) |
151 | 130, 150 | ifclda 4522 |
. . . . . . . . . . . 12
β’ ((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β if(π¦ = βͺ π¦, if(π¦ = β
, π΅, βͺ (πΊ β π¦)), ((πΊββͺ π¦) βͺ if(((πΊββͺ π¦) βͺ {(πΉββͺ π¦)}) β π΄, {(πΉββͺ π¦)}, β
))) β π΄) |
152 | 33, 151 | eqeltrd 2838 |
. . . . . . . . . . 11
β’ ((π β§ (π¦ β suc (cardβ(βͺ π΄
β π΅)) β§
βπ β π¦ (πΊβπ) β π΄)) β (πΊβπ¦) β π΄) |
153 | 152 | expr 458 |
. . . . . . . . . 10
β’ ((π β§ π¦ β suc (cardβ(βͺ π΄
β π΅))) β
(βπ β π¦ (πΊβπ) β π΄ β (πΊβπ¦) β π΄)) |
154 | 24, 153 | sylbird 260 |
. . . . . . . . 9
β’ ((π β§ π¦ β suc (cardβ(βͺ π΄
β π΅))) β
(βπ β π¦ (π β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπ) β π΄) β (πΊβπ¦) β π΄)) |
155 | 154 | ex 414 |
. . . . . . . 8
β’ (π β (π¦ β suc (cardβ(βͺ π΄
β π΅)) β
(βπ β π¦ (π β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπ) β π΄) β (πΊβπ¦) β π΄))) |
156 | 155 | com23 86 |
. . . . . . 7
β’ (π β (βπ β π¦ (π β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπ) β π΄) β (π¦ β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπ¦) β π΄))) |
157 | 156 | a2i 14 |
. . . . . 6
β’ ((π β βπ β π¦ (π β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπ) β π΄)) β (π β (π¦ β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπ¦) β π΄))) |
158 | 16, 157 | sylbi 216 |
. . . . 5
β’
(βπ β
π¦ (π β (π β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπ) β π΄)) β (π β (π¦ β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπ¦) β π΄))) |
159 | 158 | a1i 11 |
. . . 4
β’ (π¦ β On β (βπ β π¦ (π β (π β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπ) β π΄)) β (π β (π¦ β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπ¦) β π΄)))) |
160 | 10, 15, 159 | tfis3 7795 |
. . 3
β’ (πΆ β On β (π β (πΆ β suc (cardβ(βͺ π΄
β π΅)) β (πΊβπΆ) β π΄))) |
161 | 160 | impd 412 |
. 2
β’ (πΆ β On β ((π β§ πΆ β suc (cardβ(βͺ π΄
β π΅))) β (πΊβπΆ) β π΄)) |
162 | 5, 161 | mpcom 38 |
1
β’ ((π β§ πΆ β suc (cardβ(βͺ π΄
β π΅))) β (πΊβπΆ) β π΄) |