Step | Hyp | Ref
| Expression |
1 | | isinfcard 10091 |
. . . . 5
β’ ((Ο
β π΄ β§
(cardβπ΄) = π΄) β π΄ β ran β΅) |
2 | 1 | bicomi 223 |
. . . 4
β’ (π΄ β ran β΅ β
(Ο β π΄ β§
(cardβπ΄) = π΄)) |
3 | 2 | baib 535 |
. . 3
β’ (Ο
β π΄ β (π΄ β ran β΅ β
(cardβπ΄) = π΄)) |
4 | 3 | adantl 481 |
. 2
β’ ((π΄ β On β§ Ο β
π΄) β (π΄ β ran β΅ β
(cardβπ΄) = π΄)) |
5 | | onenon 9948 |
. . . . . . . 8
β’ (π΄ β On β π΄ β dom
card) |
6 | 5 | adantr 480 |
. . . . . . 7
β’ ((π΄ β On β§ Ο β
π΄) β π΄ β dom card) |
7 | | onenon 9948 |
. . . . . . 7
β’ (π₯ β On β π₯ β dom
card) |
8 | | carddom2 9976 |
. . . . . . 7
β’ ((π΄ β dom card β§ π₯ β dom card) β
((cardβπ΄) β
(cardβπ₯) β π΄ βΌ π₯)) |
9 | 6, 7, 8 | syl2an 595 |
. . . . . 6
β’ (((π΄ β On β§ Ο β
π΄) β§ π₯ β On) β ((cardβπ΄) β (cardβπ₯) β π΄ βΌ π₯)) |
10 | | cardonle 9956 |
. . . . . . . 8
β’ (π₯ β On β
(cardβπ₯) β
π₯) |
11 | 10 | adantl 481 |
. . . . . . 7
β’ (((π΄ β On β§ Ο β
π΄) β§ π₯ β On) β (cardβπ₯) β π₯) |
12 | | sstr 3990 |
. . . . . . . 8
β’
(((cardβπ΄)
β (cardβπ₯)
β§ (cardβπ₯)
β π₯) β
(cardβπ΄) β
π₯) |
13 | 12 | expcom 413 |
. . . . . . 7
β’
((cardβπ₯)
β π₯ β
((cardβπ΄) β
(cardβπ₯) β
(cardβπ΄) β
π₯)) |
14 | 11, 13 | syl 17 |
. . . . . 6
β’ (((π΄ β On β§ Ο β
π΄) β§ π₯ β On) β ((cardβπ΄) β (cardβπ₯) β (cardβπ΄) β π₯)) |
15 | 9, 14 | sylbird 260 |
. . . . 5
β’ (((π΄ β On β§ Ο β
π΄) β§ π₯ β On) β (π΄ βΌ π₯ β (cardβπ΄) β π₯)) |
16 | | sseq1 4007 |
. . . . . 6
β’
((cardβπ΄) =
π΄ β ((cardβπ΄) β π₯ β π΄ β π₯)) |
17 | 16 | imbi2d 340 |
. . . . 5
β’
((cardβπ΄) =
π΄ β ((π΄ βΌ π₯ β (cardβπ΄) β π₯) β (π΄ βΌ π₯ β π΄ β π₯))) |
18 | 15, 17 | syl5ibcom 244 |
. . . 4
β’ (((π΄ β On β§ Ο β
π΄) β§ π₯ β On) β ((cardβπ΄) = π΄ β (π΄ βΌ π₯ β π΄ β π₯))) |
19 | 18 | ralrimdva 3153 |
. . 3
β’ ((π΄ β On β§ Ο β
π΄) β
((cardβπ΄) = π΄ β βπ₯ β On (π΄ βΌ π₯ β π΄ β π₯))) |
20 | | oncardid 9955 |
. . . . . . 7
β’ (π΄ β On β
(cardβπ΄) β
π΄) |
21 | | ensym 9003 |
. . . . . . 7
β’
((cardβπ΄)
β π΄ β π΄ β (cardβπ΄)) |
22 | | endom 8979 |
. . . . . . 7
β’ (π΄ β (cardβπ΄) β π΄ βΌ (cardβπ΄)) |
23 | 20, 21, 22 | 3syl 18 |
. . . . . 6
β’ (π΄ β On β π΄ βΌ (cardβπ΄)) |
24 | 23 | adantr 480 |
. . . . 5
β’ ((π΄ β On β§ Ο β
π΄) β π΄ βΌ (cardβπ΄)) |
25 | | cardon 9943 |
. . . . . 6
β’
(cardβπ΄)
β On |
26 | | breq2 5152 |
. . . . . . . 8
β’ (π₯ = (cardβπ΄) β (π΄ βΌ π₯ β π΄ βΌ (cardβπ΄))) |
27 | | sseq2 4008 |
. . . . . . . 8
β’ (π₯ = (cardβπ΄) β (π΄ β π₯ β π΄ β (cardβπ΄))) |
28 | 26, 27 | imbi12d 344 |
. . . . . . 7
β’ (π₯ = (cardβπ΄) β ((π΄ βΌ π₯ β π΄ β π₯) β (π΄ βΌ (cardβπ΄) β π΄ β (cardβπ΄)))) |
29 | 28 | rspcv 3608 |
. . . . . 6
β’
((cardβπ΄)
β On β (βπ₯
β On (π΄ βΌ π₯ β π΄ β π₯) β (π΄ βΌ (cardβπ΄) β π΄ β (cardβπ΄)))) |
30 | 25, 29 | ax-mp 5 |
. . . . 5
β’
(βπ₯ β On
(π΄ βΌ π₯ β π΄ β π₯) β (π΄ βΌ (cardβπ΄) β π΄ β (cardβπ΄))) |
31 | 24, 30 | syl5com 31 |
. . . 4
β’ ((π΄ β On β§ Ο β
π΄) β (βπ₯ β On (π΄ βΌ π₯ β π΄ β π₯) β π΄ β (cardβπ΄))) |
32 | | cardonle 9956 |
. . . . . . 7
β’ (π΄ β On β
(cardβπ΄) β
π΄) |
33 | 32 | adantr 480 |
. . . . . 6
β’ ((π΄ β On β§ Ο β
π΄) β (cardβπ΄) β π΄) |
34 | 33 | biantrurd 532 |
. . . . 5
β’ ((π΄ β On β§ Ο β
π΄) β (π΄ β (cardβπ΄) β ((cardβπ΄) β π΄ β§ π΄ β (cardβπ΄)))) |
35 | | eqss 3997 |
. . . . 5
β’
((cardβπ΄) =
π΄ β ((cardβπ΄) β π΄ β§ π΄ β (cardβπ΄))) |
36 | 34, 35 | bitr4di 289 |
. . . 4
β’ ((π΄ β On β§ Ο β
π΄) β (π΄ β (cardβπ΄) β (cardβπ΄) = π΄)) |
37 | 31, 36 | sylibd 238 |
. . 3
β’ ((π΄ β On β§ Ο β
π΄) β (βπ₯ β On (π΄ βΌ π₯ β π΄ β π₯) β (cardβπ΄) = π΄)) |
38 | 19, 37 | impbid 211 |
. 2
β’ ((π΄ β On β§ Ο β
π΄) β
((cardβπ΄) = π΄ β βπ₯ β On (π΄ βΌ π₯ β π΄ β π₯))) |
39 | 4, 38 | bitrd 279 |
1
β’ ((π΄ β On β§ Ο β
π΄) β (π΄ β ran β΅ β
βπ₯ β On (π΄ βΌ π₯ β π΄ β π₯))) |