Step | Hyp | Ref
| Expression |
1 | | eldif 3921 |
. . . . . . 7
β’ (π΄ β (ran card β
Ο) β (π΄ β
ran card β§ Β¬ π΄
β Ο)) |
2 | | omelon 9583 |
. . . . . . . . . 10
β’ Ο
β On |
3 | | cardon 9881 |
. . . . . . . . . . 11
β’
(cardβπ΄)
β On |
4 | | eleq1 2826 |
. . . . . . . . . . 11
β’
((cardβπ΄) =
π΄ β ((cardβπ΄) β On β π΄ β On)) |
5 | 3, 4 | mpbii 232 |
. . . . . . . . . 10
β’
((cardβπ΄) =
π΄ β π΄ β On) |
6 | | ontri1 6352 |
. . . . . . . . . 10
β’ ((Ο
β On β§ π΄ β
On) β (Ο β π΄ β Β¬ π΄ β Ο)) |
7 | 2, 5, 6 | sylancr 588 |
. . . . . . . . 9
β’
((cardβπ΄) =
π΄ β (Ο β
π΄ β Β¬ π΄ β
Ο)) |
8 | 7 | pm5.32i 576 |
. . . . . . . 8
β’
(((cardβπ΄) =
π΄ β§ Ο β
π΄) β
((cardβπ΄) = π΄ β§ Β¬ π΄ β Ο)) |
9 | | iscard4 41812 |
. . . . . . . . 9
β’
((cardβπ΄) =
π΄ β π΄ β ran card) |
10 | 9 | anbi1i 625 |
. . . . . . . 8
β’
(((cardβπ΄) =
π΄ β§ Β¬ π΄ β Ο) β (π΄ β ran card β§ Β¬
π΄ β
Ο)) |
11 | 8, 10 | bitr2i 276 |
. . . . . . 7
β’ ((π΄ β ran card β§ Β¬
π΄ β Ο) β
((cardβπ΄) = π΄ β§ Ο β π΄)) |
12 | | ancom 462 |
. . . . . . 7
β’
(((cardβπ΄) =
π΄ β§ Ο β
π΄) β (Ο β
π΄ β§ (cardβπ΄) = π΄)) |
13 | 1, 11, 12 | 3bitri 297 |
. . . . . 6
β’ (π΄ β (ran card β
Ο) β (Ο β π΄ β§ (cardβπ΄) = π΄)) |
14 | 13 | biimpi 215 |
. . . . 5
β’ (π΄ β (ran card β
Ο) β (Ο β π΄ β§ (cardβπ΄) = π΄)) |
15 | | cardalephex 10027 |
. . . . . . . 8
β’ (Ο
β π΄ β
((cardβπ΄) = π΄ β βπ₯ β On π΄ = (β΅βπ₯))) |
16 | 15 | biimpa 478 |
. . . . . . 7
β’ ((Ο
β π΄ β§
(cardβπ΄) = π΄) β βπ₯ β On π΄ = (β΅βπ₯)) |
17 | | eqimss 4001 |
. . . . . . . . 9
β’ (π΄ = (β΅βπ₯) β π΄ β (β΅βπ₯)) |
18 | 17 | a1i 11 |
. . . . . . . 8
β’ ((Ο
β π΄ β§
(cardβπ΄) = π΄) β (π΄ = (β΅βπ₯) β π΄ β (β΅βπ₯))) |
19 | 18 | reximdv 3168 |
. . . . . . 7
β’ ((Ο
β π΄ β§
(cardβπ΄) = π΄) β (βπ₯ β On π΄ = (β΅βπ₯) β βπ₯ β On π΄ β (β΅βπ₯))) |
20 | 16, 19 | mpd 15 |
. . . . . 6
β’ ((Ο
β π΄ β§
(cardβπ΄) = π΄) β βπ₯ β On π΄ β (β΅βπ₯)) |
21 | | onintrab2 7733 |
. . . . . 6
β’
(βπ₯ β On
π΄ β
(β΅βπ₯) β
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On) |
22 | 20, 21 | sylib 217 |
. . . . 5
β’ ((Ο
β π΄ β§
(cardβπ΄) = π΄) β β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On) |
23 | | simpr 486 |
. . . . . . 7
β’
(((Ο β π΄
β§ (cardβπ΄) =
π΄) β§ β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On) β β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On) |
24 | | onsuc 7747 |
. . . . . . 7
β’ (β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On β suc β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On) |
25 | 23, 24 | syl 17 |
. . . . . 6
β’
(((Ο β π΄
β§ (cardβπ΄) =
π΄) β§ β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On) β suc β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On) |
26 | | eloni 6328 |
. . . . . . . . 9
β’ (β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On β Ord β© {π₯ β On β£ π΄ β (β΅βπ₯)}) |
27 | 23, 26 | syl 17 |
. . . . . . . 8
β’
(((Ο β π΄
β§ (cardβπ΄) =
π΄) β§ β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On) β Ord β© {π₯ β On β£ π΄ β (β΅βπ₯)}) |
28 | | 0elsuc 7771 |
. . . . . . . 8
β’ (Ord
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β β
β suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)}) |
29 | 27, 28 | syl 17 |
. . . . . . 7
β’
(((Ο β π΄
β§ (cardβπ΄) =
π΄) β§ β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On) β β
β suc β© {π₯ β On β£ π΄ β (β΅βπ₯)}) |
30 | | cardaleph 10026 |
. . . . . . . . 9
β’ ((Ο
β π΄ β§
(cardβπ΄) = π΄) β π΄ = (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)})) |
31 | 30 | adantr 482 |
. . . . . . . 8
β’
(((Ο β π΄
β§ (cardβπ΄) =
π΄) β§ β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On) β π΄ =
(β΅ββ© {π₯ β On β£ π΄ β (β΅βπ₯)})) |
32 | | sssucid 6398 |
. . . . . . . . 9
β’ β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
suc β© {π₯ β On β£ π΄ β (β΅βπ₯)} |
33 | | alephord3 10015 |
. . . . . . . . . 10
β’ ((β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On β§ suc β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On) β (β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
suc β© {π₯ β On β£ π΄ β (β΅βπ₯)} β (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
(β΅βsuc β© {π₯ β On β£ π΄ β (β΅βπ₯)}))) |
34 | 23, 24, 33 | syl2anc2 586 |
. . . . . . . . 9
β’
(((Ο β π΄
β§ (cardβπ΄) =
π΄) β§ β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On) β (β© {π₯ β On β£ π΄ β (β΅βπ₯)} β suc β©
{π₯ β On β£ π΄ β (β΅βπ₯)} β (β΅ββ© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β
(β΅βsuc β© {π₯ β On β£ π΄ β (β΅βπ₯)}))) |
35 | 32, 34 | mpbii 232 |
. . . . . . . 8
β’
(((Ο β π΄
β§ (cardβπ΄) =
π΄) β§ β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On) β (β΅ββ© {π₯ β On β£ π΄ β (β΅βπ₯)}) β (β΅βsuc β© {π₯
β On β£ π΄ β
(β΅βπ₯)})) |
36 | 31, 35 | eqsstrd 3983 |
. . . . . . 7
β’
(((Ο β π΄
β§ (cardβπ΄) =
π΄) β§ β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On) β π΄ β
(β΅βsuc β© {π₯ β On β£ π΄ β (β΅βπ₯)})) |
37 | | alephreg 10519 |
. . . . . . . 8
β’
(cfβ(β΅βsuc β© {π₯ β On β£ π΄ β (β΅βπ₯)})) = (β΅βsuc β© {π₯
β On β£ π΄ β
(β΅βπ₯)}) |
38 | 37 | a1i 11 |
. . . . . . 7
β’
(((Ο β π΄
β§ (cardβπ΄) =
π΄) β§ β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On) β (cfβ(β΅βsuc β© {π₯ β On β£ π΄ β (β΅βπ₯)})) = (β΅βsuc β© {π₯
β On β£ π΄ β
(β΅βπ₯)})) |
39 | 29, 36, 38 | 3jca 1129 |
. . . . . 6
β’
(((Ο β π΄
β§ (cardβπ΄) =
π΄) β§ β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On) β (β
β suc β© {π₯ β On β£ π΄ β (β΅βπ₯)} β§ π΄ β (β΅βsuc β© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β§
(cfβ(β΅βsuc β© {π₯ β On β£ π΄ β (β΅βπ₯)})) = (β΅βsuc β© {π₯
β On β£ π΄ β
(β΅βπ₯)}))) |
40 | 25, 39 | jca 513 |
. . . . 5
β’
(((Ο β π΄
β§ (cardβπ΄) =
π΄) β§ β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On) β (suc β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On β§ (β
β suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β§
π΄ β
(β΅βsuc β© {π₯ β On β£ π΄ β (β΅βπ₯)}) β§ (cfβ(β΅βsuc β© {π₯
β On β£ π΄ β
(β΅βπ₯)})) =
(β΅βsuc β© {π₯ β On β£ π΄ β (β΅βπ₯)})))) |
41 | 14, 22, 40 | syl2anc2 586 |
. . . 4
β’ (π΄ β (ran card β
Ο) β (suc β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On β§ (β
β suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β§
π΄ β
(β΅βsuc β© {π₯ β On β£ π΄ β (β΅βπ₯)}) β§ (cfβ(β΅βsuc β© {π₯
β On β£ π΄ β
(β΅βπ₯)})) =
(β΅βsuc β© {π₯ β On β£ π΄ β (β΅βπ₯)})))) |
42 | 14, 16 | syl 17 |
. . . . . . . 8
β’ (π΄ β (ran card β
Ο) β βπ₯
β On π΄ =
(β΅βπ₯)) |
43 | 17 | a1i 11 |
. . . . . . . . 9
β’ (π΄ β (ran card β
Ο) β (π΄ =
(β΅βπ₯) β
π΄ β
(β΅βπ₯))) |
44 | 43 | reximdv 3168 |
. . . . . . . 8
β’ (π΄ β (ran card β
Ο) β (βπ₯
β On π΄ =
(β΅βπ₯) β
βπ₯ β On π΄ β (β΅βπ₯))) |
45 | 42, 44 | mpd 15 |
. . . . . . 7
β’ (π΄ β (ran card β
Ο) β βπ₯
β On π΄ β
(β΅βπ₯)) |
46 | 45, 21 | sylib 217 |
. . . . . 6
β’ (π΄ β (ran card β
Ο) β β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On) |
47 | 46, 24 | syl 17 |
. . . . 5
β’ (π΄ β (ran card β
Ο) β suc β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On) |
48 | | sbcan 3792 |
. . . . . 6
β’
([suc β© {π₯ β On β£ π΄ β (β΅βπ₯)} / π¦](π¦ β On β§ (β
β π¦ β§ π΄ β (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦))) β ([suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦]π¦ β On β§ [suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦](β
β π¦ β§ π΄ β (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦)))) |
49 | | sbcel1v 3811 |
. . . . . . . 8
β’
([suc β© {π₯ β On β£ π΄ β (β΅βπ₯)} / π¦]π¦ β On β suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On) |
50 | 49 | a1i 11 |
. . . . . . 7
β’ (suc
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On β ([suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦]π¦ β On β suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On)) |
51 | | sbc3an 3810 |
. . . . . . . 8
β’
([suc β© {π₯ β On β£ π΄ β (β΅βπ₯)} / π¦](β
β π¦ β§ π΄ β (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦)) β ([suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦]β
β π¦ β§ [suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦]π΄ β (β΅βπ¦) β§ [suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦](cfβ(β΅βπ¦)) = (β΅βπ¦))) |
52 | | sbcel2gv 3812 |
. . . . . . . . 9
β’ (suc
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On β ([suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦]β
β π¦ β β
β suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)})) |
53 | | sbcssg 4482 |
. . . . . . . . . 10
β’ (suc
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On β ([suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦]π΄ β (β΅βπ¦) β β¦suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦β¦π΄ β β¦suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦β¦(β΅βπ¦))) |
54 | | csbconstg 3875 |
. . . . . . . . . . 11
β’ (suc
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On β β¦suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦β¦π΄ = π΄) |
55 | | csbfv2g 6892 |
. . . . . . . . . . . 12
β’ (suc
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On β β¦suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦β¦(β΅βπ¦) =
(β΅ββ¦suc β© {π₯ β On β£ π΄ β (β΅βπ₯)} / π¦β¦π¦)) |
56 | | csbvarg 4392 |
. . . . . . . . . . . . 13
β’ (suc
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On β β¦suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦β¦π¦ = suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)}) |
57 | 56 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (suc
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On β
(β΅ββ¦suc β© {π₯ β On β£ π΄ β (β΅βπ₯)} / π¦β¦π¦) = (β΅βsuc β© {π₯
β On β£ π΄ β
(β΅βπ₯)})) |
58 | 55, 57 | eqtrd 2777 |
. . . . . . . . . . 11
β’ (suc
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On β β¦suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦β¦(β΅βπ¦) = (β΅βsuc β© {π₯
β On β£ π΄ β
(β΅βπ₯)})) |
59 | 54, 58 | sseq12d 3978 |
. . . . . . . . . 10
β’ (suc
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On β (β¦suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦β¦π΄ β β¦suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦β¦(β΅βπ¦) β π΄ β (β΅βsuc β© {π₯
β On β£ π΄ β
(β΅βπ₯)}))) |
60 | 53, 59 | bitrd 279 |
. . . . . . . . 9
β’ (suc
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On β ([suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦]π΄ β (β΅βπ¦) β π΄ β (β΅βsuc β© {π₯
β On β£ π΄ β
(β΅βπ₯)}))) |
61 | | sbceqg 4370 |
. . . . . . . . . 10
β’ (suc
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On β ([suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦](cfβ(β΅βπ¦)) = (β΅βπ¦) β β¦suc
β© {π₯ β On β£ π΄ β (β΅βπ₯)} / π¦β¦(cfβ(β΅βπ¦)) = β¦suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦β¦(β΅βπ¦))) |
62 | | csbfv2g 6892 |
. . . . . . . . . . . 12
β’ (suc
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On β β¦suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦β¦(cfβ(β΅βπ¦)) =
(cfββ¦suc β© {π₯ β On β£ π΄ β (β΅βπ₯)} / π¦β¦(β΅βπ¦))) |
63 | 58 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (suc
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On β
(cfββ¦suc β© {π₯ β On β£ π΄ β (β΅βπ₯)} / π¦β¦(β΅βπ¦)) =
(cfβ(β΅βsuc β© {π₯ β On β£ π΄ β (β΅βπ₯)}))) |
64 | 62, 63 | eqtrd 2777 |
. . . . . . . . . . 11
β’ (suc
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On β β¦suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦β¦(cfβ(β΅βπ¦)) =
(cfβ(β΅βsuc β© {π₯ β On β£ π΄ β (β΅βπ₯)}))) |
65 | 64, 58 | eqeq12d 2753 |
. . . . . . . . . 10
β’ (suc
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On β (β¦suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦β¦(cfβ(β΅βπ¦)) = β¦suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦β¦(β΅βπ¦) β
(cfβ(β΅βsuc β© {π₯ β On β£ π΄ β (β΅βπ₯)})) = (β΅βsuc β© {π₯
β On β£ π΄ β
(β΅βπ₯)}))) |
66 | 61, 65 | bitrd 279 |
. . . . . . . . 9
β’ (suc
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On β ([suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦](cfβ(β΅βπ¦)) = (β΅βπ¦) β
(cfβ(β΅βsuc β© {π₯ β On β£ π΄ β (β΅βπ₯)})) = (β΅βsuc β© {π₯
β On β£ π΄ β
(β΅βπ₯)}))) |
67 | 52, 60, 66 | 3anbi123d 1437 |
. . . . . . . 8
β’ (suc
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On β (([suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦]β
β π¦ β§ [suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦]π΄ β (β΅βπ¦) β§ [suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦](cfβ(β΅βπ¦)) = (β΅βπ¦)) β (β
β suc
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β§ π΄ β (β΅βsuc β© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β§
(cfβ(β΅βsuc β© {π₯ β On β£ π΄ β (β΅βπ₯)})) = (β΅βsuc β© {π₯
β On β£ π΄ β
(β΅βπ₯)})))) |
68 | 51, 67 | bitrid 283 |
. . . . . . 7
β’ (suc
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On β ([suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦](β
β π¦ β§ π΄ β (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦)) β (β
β suc
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β§ π΄ β (β΅βsuc β© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β§
(cfβ(β΅βsuc β© {π₯ β On β£ π΄ β (β΅βπ₯)})) = (β΅βsuc β© {π₯
β On β£ π΄ β
(β΅βπ₯)})))) |
69 | 50, 68 | anbi12d 632 |
. . . . . 6
β’ (suc
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On β (([suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦]π¦ β On β§ [suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦](β
β π¦ β§ π΄ β (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦))) β (suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On β§ (β
β suc β© {π₯ β On β£ π΄ β (β΅βπ₯)} β§ π΄ β (β΅βsuc β© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β§
(cfβ(β΅βsuc β© {π₯ β On β£ π΄ β (β΅βπ₯)})) = (β΅βsuc β© {π₯
β On β£ π΄ β
(β΅βπ₯)}))))) |
70 | 48, 69 | bitrid 283 |
. . . . 5
β’ (suc
β© {π₯ β On β£ π΄ β (β΅βπ₯)} β On β ([suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} / π¦](π¦ β On β§ (β
β π¦ β§ π΄ β (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦))) β (suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On β§ (β
β suc β© {π₯ β On β£ π΄ β (β΅βπ₯)} β§ π΄ β (β΅βsuc β© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β§
(cfβ(β΅βsuc β© {π₯ β On β£ π΄ β (β΅βπ₯)})) = (β΅βsuc β© {π₯
β On β£ π΄ β
(β΅βπ₯)}))))) |
71 | 47, 70 | syl 17 |
. . . 4
β’ (π΄ β (ran card β
Ο) β ([suc β© {π₯ β On β£ π΄ β (β΅βπ₯)} / π¦](π¦ β On β§ (β
β π¦ β§ π΄ β (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦))) β (suc β© {π₯
β On β£ π΄ β
(β΅βπ₯)} β
On β§ (β
β suc β© {π₯ β On β£ π΄ β (β΅βπ₯)} β§ π΄ β (β΅βsuc β© {π₯
β On β£ π΄ β
(β΅βπ₯)}) β§
(cfβ(β΅βsuc β© {π₯ β On β£ π΄ β (β΅βπ₯)})) = (β΅βsuc β© {π₯
β On β£ π΄ β
(β΅βπ₯)}))))) |
72 | 41, 71 | mpbird 257 |
. . 3
β’ (π΄ β (ran card β
Ο) β [suc β© {π₯ β On β£ π΄ β (β΅βπ₯)} / π¦](π¦ β On β§ (β
β π¦ β§ π΄ β (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦)))) |
73 | 72 | spesbcd 3840 |
. 2
β’ (π΄ β (ran card β
Ο) β βπ¦(π¦ β On β§ (β
β π¦ β§ π΄ β (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦)))) |
74 | | onintrab2 7733 |
. . 3
β’
(βπ¦ β On
(β
β π¦ β§
π΄ β
(β΅βπ¦) β§
(cfβ(β΅βπ¦)) = (β΅βπ¦)) β β© {π¦ β On β£ (β
β π¦ β§ π΄ β (β΅βπ¦) β§
(cfβ(β΅βπ¦)) = (β΅βπ¦))} β On) |
75 | | df-rex 3075 |
. . 3
β’
(βπ¦ β On
(β
β π¦ β§
π΄ β
(β΅βπ¦) β§
(cfβ(β΅βπ¦)) = (β΅βπ¦)) β βπ¦(π¦ β On β§ (β
β π¦ β§ π΄ β (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦)))) |
76 | | risset 3222 |
. . 3
β’ (β© {π¦
β On β£ (β
β π¦ β§ π΄ β (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦))} β On β
βπ₯ β On π₯ = β©
{π¦ β On β£
(β
β π¦ β§
π΄ β
(β΅βπ¦) β§
(cfβ(β΅βπ¦)) = (β΅βπ¦))}) |
77 | 74, 75, 76 | 3bitr3i 301 |
. 2
β’
(βπ¦(π¦ β On β§ (β
β
π¦ β§ π΄ β (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦))) β βπ₯ β On π₯ = β© {π¦ β On β£ (β
β π¦ β§ π΄ β (β΅βπ¦) β§
(cfβ(β΅βπ¦)) = (β΅βπ¦))}) |
78 | 73, 77 | sylib 217 |
1
β’ (π΄ β (ran card β
Ο) β βπ₯
β On π₯ = β© {π¦
β On β£ (β
β π¦ β§ π΄ β (β΅βπ¦) β§ (cfβ(β΅βπ¦)) = (β΅βπ¦))}) |