Step | Hyp | Ref
| Expression |
1 | | cardf2 9880 |
. . . . . . 7
β’
card:{π₯ β£
βπ¦ β On π¦ β π₯}βΆOn |
2 | | ffun 6672 |
. . . . . . 7
β’
(card:{π₯ β£
βπ¦ β On π¦ β π₯}βΆOn β Fun card) |
3 | 1, 2 | ax-mp 5 |
. . . . . 6
β’ Fun
card |
4 | | r1fnon 9704 |
. . . . . . 7
β’
π
1 Fn On |
5 | | fnfun 6603 |
. . . . . . 7
β’
(π
1 Fn On β Fun
π
1) |
6 | 4, 5 | ax-mp 5 |
. . . . . 6
β’ Fun
π
1 |
7 | | funco 6542 |
. . . . . 6
β’ ((Fun
card β§ Fun π
1) β Fun (card β
π
1)) |
8 | 3, 6, 7 | mp2an 691 |
. . . . 5
β’ Fun (card
β π
1) |
9 | | funfn 6532 |
. . . . 5
β’ (Fun
(card β π
1) β (card β
π
1) Fn dom (card β
π
1)) |
10 | 8, 9 | mpbi 229 |
. . . 4
β’ (card
β π
1) Fn dom (card β
π
1) |
11 | | rnco 6205 |
. . . . 5
β’ ran (card
β π
1) = ran (card βΎ ran
π
1) |
12 | | resss 5963 |
. . . . . . 7
β’ (card
βΎ ran π
1) β card |
13 | 12 | rnssi 5896 |
. . . . . 6
β’ ran (card
βΎ ran π
1) β ran card |
14 | | frn 6676 |
. . . . . . 7
β’
(card:{π₯ β£
βπ¦ β On π¦ β π₯}βΆOn β ran card β
On) |
15 | 1, 14 | ax-mp 5 |
. . . . . 6
β’ ran card
β On |
16 | 13, 15 | sstri 3954 |
. . . . 5
β’ ran (card
βΎ ran π
1) β On |
17 | 11, 16 | eqsstri 3979 |
. . . 4
β’ ran (card
β π
1) β On |
18 | | df-f 6501 |
. . . 4
β’ ((card
β π
1):dom (card β
π
1)βΆOn β ((card β π
1)
Fn dom (card β π
1) β§ ran (card β
π
1) β On)) |
19 | 10, 17, 18 | mpbir2an 710 |
. . 3
β’ (card
β π
1):dom (card β
π
1)βΆOn |
20 | | dmco 6207 |
. . . 4
β’ dom (card
β π
1) = (β‘π
1 β dom
card) |
21 | 20 | feq2i 6661 |
. . 3
β’ ((card
β π
1):dom (card β
π
1)βΆOn β (card β
π
1):(β‘π
1 β dom
card)βΆOn) |
22 | 19, 21 | mpbi 229 |
. 2
β’ (card
β π
1):(β‘π
1 β dom
card)βΆOn |
23 | | elpreima 7009 |
. . . . . . . . 9
β’
(π
1 Fn On β (π₯ β (β‘π
1 β dom card)
β (π₯ β On β§
(π
1βπ₯) β dom card))) |
24 | 4, 23 | ax-mp 5 |
. . . . . . . 8
β’ (π₯ β (β‘π
1 β dom card)
β (π₯ β On β§
(π
1βπ₯) β dom card)) |
25 | 24 | simplbi 499 |
. . . . . . 7
β’ (π₯ β (β‘π
1 β dom card)
β π₯ β
On) |
26 | | onelon 6343 |
. . . . . . 7
β’ ((π₯ β On β§ π¦ β π₯) β π¦ β On) |
27 | 25, 26 | sylan 581 |
. . . . . 6
β’ ((π₯ β (β‘π
1 β dom card)
β§ π¦ β π₯) β π¦ β On) |
28 | 24 | simprbi 498 |
. . . . . . . 8
β’ (π₯ β (β‘π
1 β dom card)
β (π
1βπ₯) β dom card) |
29 | 28 | adantr 482 |
. . . . . . 7
β’ ((π₯ β (β‘π
1 β dom card)
β§ π¦ β π₯) β
(π
1βπ₯) β dom card) |
30 | | r1ord2 9718 |
. . . . . . . . 9
β’ (π₯ β On β (π¦ β π₯ β (π
1βπ¦) β
(π
1βπ₯))) |
31 | 30 | imp 408 |
. . . . . . . 8
β’ ((π₯ β On β§ π¦ β π₯) β (π
1βπ¦) β
(π
1βπ₯)) |
32 | 25, 31 | sylan 581 |
. . . . . . 7
β’ ((π₯ β (β‘π
1 β dom card)
β§ π¦ β π₯) β
(π
1βπ¦) β (π
1βπ₯)) |
33 | | ssnum 9976 |
. . . . . . 7
β’
(((π
1βπ₯) β dom card β§
(π
1βπ¦) β (π
1βπ₯)) β
(π
1βπ¦) β dom card) |
34 | 29, 32, 33 | syl2anc 585 |
. . . . . 6
β’ ((π₯ β (β‘π
1 β dom card)
β§ π¦ β π₯) β
(π
1βπ¦) β dom card) |
35 | | elpreima 7009 |
. . . . . . 7
β’
(π
1 Fn On β (π¦ β (β‘π
1 β dom card)
β (π¦ β On β§
(π
1βπ¦) β dom card))) |
36 | 4, 35 | ax-mp 5 |
. . . . . 6
β’ (π¦ β (β‘π
1 β dom card)
β (π¦ β On β§
(π
1βπ¦) β dom card)) |
37 | 27, 34, 36 | sylanbrc 584 |
. . . . 5
β’ ((π₯ β (β‘π
1 β dom card)
β§ π¦ β π₯) β π¦ β (β‘π
1 β dom
card)) |
38 | 37 | rgen2 3195 |
. . . 4
β’
βπ₯ β
(β‘π
1 β dom
card)βπ¦ β π₯ π¦ β (β‘π
1 β dom
card) |
39 | | dftr5 5227 |
. . . 4
β’ (Tr
(β‘π
1 β dom
card) β βπ₯
β (β‘π
1 β
dom card)βπ¦ β
π₯ π¦ β (β‘π
1 β dom
card)) |
40 | 38, 39 | mpbir 230 |
. . 3
β’ Tr (β‘π
1 β dom
card) |
41 | | cnvimass 6034 |
. . . . 5
β’ (β‘π
1 β dom card)
β dom π
1 |
42 | | dffn2 6671 |
. . . . . . 7
β’
(π
1 Fn On β
π
1:OnβΆV) |
43 | 4, 42 | mpbi 229 |
. . . . . 6
β’
π
1:OnβΆV |
44 | 43 | fdmi 6681 |
. . . . 5
β’ dom
π
1 = On |
45 | 41, 44 | sseqtri 3981 |
. . . 4
β’ (β‘π
1 β dom card)
β On |
46 | | epweon 7710 |
. . . 4
β’ E We
On |
47 | | wess 5621 |
. . . 4
β’ ((β‘π
1 β dom card)
β On β ( E We On β E We (β‘π
1 β dom
card))) |
48 | 45, 46, 47 | mp2 9 |
. . 3
β’ E We
(β‘π
1 β dom
card) |
49 | | df-ord 6321 |
. . 3
β’ (Ord
(β‘π
1 β dom
card) β (Tr (β‘π
1 β dom card)
β§ E We (β‘π
1
β dom card))) |
50 | 40, 48, 49 | mpbir2an 710 |
. 2
β’ Ord
(β‘π
1 β dom
card) |
51 | | r1sdom 9711 |
. . . . . . 7
β’ ((π₯ β On β§ π¦ β π₯) β (π
1βπ¦) βΊ
(π
1βπ₯)) |
52 | 25, 51 | sylan 581 |
. . . . . 6
β’ ((π₯ β (β‘π
1 β dom card)
β§ π¦ β π₯) β
(π
1βπ¦) βΊ (π
1βπ₯)) |
53 | | cardsdom2 9925 |
. . . . . . 7
β’
(((π
1βπ¦) β dom card β§
(π
1βπ₯) β dom card) β
((cardβ(π
1βπ¦)) β
(cardβ(π
1βπ₯)) β (π
1βπ¦) βΊ
(π
1βπ₯))) |
54 | 34, 29, 53 | syl2anc 585 |
. . . . . 6
β’ ((π₯ β (β‘π
1 β dom card)
β§ π¦ β π₯) β
((cardβ(π
1βπ¦)) β
(cardβ(π
1βπ₯)) β (π
1βπ¦) βΊ
(π
1βπ₯))) |
55 | 52, 54 | mpbird 257 |
. . . . 5
β’ ((π₯ β (β‘π
1 β dom card)
β§ π¦ β π₯) β
(cardβ(π
1βπ¦)) β
(cardβ(π
1βπ₯))) |
56 | | fvco2 6939 |
. . . . . 6
β’
((π
1 Fn On β§ π¦ β On) β ((card β
π
1)βπ¦) =
(cardβ(π
1βπ¦))) |
57 | 4, 27, 56 | sylancr 588 |
. . . . 5
β’ ((π₯ β (β‘π
1 β dom card)
β§ π¦ β π₯) β ((card β
π
1)βπ¦) =
(cardβ(π
1βπ¦))) |
58 | 25 | adantr 482 |
. . . . . 6
β’ ((π₯ β (β‘π
1 β dom card)
β§ π¦ β π₯) β π₯ β On) |
59 | | fvco2 6939 |
. . . . . 6
β’
((π
1 Fn On β§ π₯ β On) β ((card β
π
1)βπ₯) =
(cardβ(π
1βπ₯))) |
60 | 4, 58, 59 | sylancr 588 |
. . . . 5
β’ ((π₯ β (β‘π
1 β dom card)
β§ π¦ β π₯) β ((card β
π
1)βπ₯) =
(cardβ(π
1βπ₯))) |
61 | 55, 57, 60 | 3eltr4d 2853 |
. . . 4
β’ ((π₯ β (β‘π
1 β dom card)
β§ π¦ β π₯) β ((card β
π
1)βπ¦) β ((card β
π
1)βπ₯)) |
62 | 61 | ex 414 |
. . 3
β’ (π₯ β (β‘π
1 β dom card)
β (π¦ β π₯ β ((card β
π
1)βπ¦) β ((card β
π
1)βπ₯))) |
63 | 62 | adantl 483 |
. 2
β’ ((π¦ β (β‘π
1 β dom card)
β§ π₯ β (β‘π
1 β dom card))
β (π¦ β π₯ β ((card β
π
1)βπ¦) β ((card β
π
1)βπ₯))) |
64 | 22, 50, 63, 20 | issmo 8295 |
1
β’ Smo (card
β π
1) |