Step | Hyp | Ref
| Expression |
1 | | frn 6722 |
. . . . . . 7
β’ (π:π΅βΆπ΄ β ran π β π΄) |
2 | 1 | adantr 482 |
. . . . . 6
β’ ((π:π΅βΆπ΄ β§ βπ§ β π΄ βπ€ β π΅ π§ β (πβπ€)) β ran π β π΄) |
3 | | ffn 6715 |
. . . . . . . . . . 11
β’ (π:π΅βΆπ΄ β π Fn π΅) |
4 | | fnfvelrn 7080 |
. . . . . . . . . . 11
β’ ((π Fn π΅ β§ π€ β π΅) β (πβπ€) β ran π) |
5 | 3, 4 | sylan 581 |
. . . . . . . . . 10
β’ ((π:π΅βΆπ΄ β§ π€ β π΅) β (πβπ€) β ran π) |
6 | | sseq2 4008 |
. . . . . . . . . . 11
β’ (π = (πβπ€) β (π§ β π β π§ β (πβπ€))) |
7 | 6 | rspcev 3613 |
. . . . . . . . . 10
β’ (((πβπ€) β ran π β§ π§ β (πβπ€)) β βπ β ran π π§ β π ) |
8 | 5, 7 | sylan 581 |
. . . . . . . . 9
β’ (((π:π΅βΆπ΄ β§ π€ β π΅) β§ π§ β (πβπ€)) β βπ β ran π π§ β π ) |
9 | 8 | rexlimdva2 3158 |
. . . . . . . 8
β’ (π:π΅βΆπ΄ β (βπ€ β π΅ π§ β (πβπ€) β βπ β ran π π§ β π )) |
10 | 9 | ralimdv 3170 |
. . . . . . 7
β’ (π:π΅βΆπ΄ β (βπ§ β π΄ βπ€ β π΅ π§ β (πβπ€) β βπ§ β π΄ βπ β ran π π§ β π )) |
11 | 10 | imp 408 |
. . . . . 6
β’ ((π:π΅βΆπ΄ β§ βπ§ β π΄ βπ€ β π΅ π§ β (πβπ€)) β βπ§ β π΄ βπ β ran π π§ β π ) |
12 | 2, 11 | jca 513 |
. . . . 5
β’ ((π:π΅βΆπ΄ β§ βπ§ β π΄ βπ€ β π΅ π§ β (πβπ€)) β (ran π β π΄ β§ βπ§ β π΄ βπ β ran π π§ β π )) |
13 | | fvex 6902 |
. . . . . 6
β’
(cardβran π)
β V |
14 | | cfval 10239 |
. . . . . . . . . . 11
β’ (π΄ β On β
(cfβπ΄) = β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ β π¦ π§ β π ))}) |
15 | 14 | adantr 482 |
. . . . . . . . . 10
β’ ((π΄ β On β§ π΅ β On) β
(cfβπ΄) = β© {π₯
β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ β π¦ π§ β π ))}) |
16 | 15 | 3ad2ant2 1135 |
. . . . . . . . 9
β’ ((π₯ = (cardβran π) β§ (π΄ β On β§ π΅ β On) β§ (ran π β π΄ β§ βπ§ β π΄ βπ β ran π π§ β π )) β (cfβπ΄) = β© {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ β π¦ π§ β π ))}) |
17 | | vex 3479 |
. . . . . . . . . . . . . 14
β’ π β V |
18 | 17 | rnex 7900 |
. . . . . . . . . . . . 13
β’ ran π β V |
19 | | fveq2 6889 |
. . . . . . . . . . . . . . 15
β’ (π¦ = ran π β (cardβπ¦) = (cardβran π)) |
20 | 19 | eqeq2d 2744 |
. . . . . . . . . . . . . 14
β’ (π¦ = ran π β (π₯ = (cardβπ¦) β π₯ = (cardβran π))) |
21 | | sseq1 4007 |
. . . . . . . . . . . . . . 15
β’ (π¦ = ran π β (π¦ β π΄ β ran π β π΄)) |
22 | | rexeq 3322 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = ran π β (βπ β π¦ π§ β π β βπ β ran π π§ β π )) |
23 | 22 | ralbidv 3178 |
. . . . . . . . . . . . . . 15
β’ (π¦ = ran π β (βπ§ β π΄ βπ β π¦ π§ β π β βπ§ β π΄ βπ β ran π π§ β π )) |
24 | 21, 23 | anbi12d 632 |
. . . . . . . . . . . . . 14
β’ (π¦ = ran π β ((π¦ β π΄ β§ βπ§ β π΄ βπ β π¦ π§ β π ) β (ran π β π΄ β§ βπ§ β π΄ βπ β ran π π§ β π ))) |
25 | 20, 24 | anbi12d 632 |
. . . . . . . . . . . . 13
β’ (π¦ = ran π β ((π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ β π¦ π§ β π )) β (π₯ = (cardβran π) β§ (ran π β π΄ β§ βπ§ β π΄ βπ β ran π π§ β π )))) |
26 | 18, 25 | spcev 3597 |
. . . . . . . . . . . 12
β’ ((π₯ = (cardβran π) β§ (ran π β π΄ β§ βπ§ β π΄ βπ β ran π π§ β π )) β βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ β π¦ π§ β π ))) |
27 | | abid 2714 |
. . . . . . . . . . . 12
β’ (π₯ β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ β π¦ π§ β π ))} β βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ β π¦ π§ β π ))) |
28 | 26, 27 | sylibr 233 |
. . . . . . . . . . 11
β’ ((π₯ = (cardβran π) β§ (ran π β π΄ β§ βπ§ β π΄ βπ β ran π π§ β π )) β π₯ β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ β π¦ π§ β π ))}) |
29 | | intss1 4967 |
. . . . . . . . . . 11
β’ (π₯ β {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ β π¦ π§ β π ))} β β©
{π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ β π¦ π§ β π ))} β π₯) |
30 | 28, 29 | syl 17 |
. . . . . . . . . 10
β’ ((π₯ = (cardβran π) β§ (ran π β π΄ β§ βπ§ β π΄ βπ β ran π π§ β π )) β β© {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ β π¦ π§ β π ))} β π₯) |
31 | 30 | 3adant2 1132 |
. . . . . . . . 9
β’ ((π₯ = (cardβran π) β§ (π΄ β On β§ π΅ β On) β§ (ran π β π΄ β§ βπ§ β π΄ βπ β ran π π§ β π )) β β© {π₯ β£ βπ¦(π₯ = (cardβπ¦) β§ (π¦ β π΄ β§ βπ§ β π΄ βπ β π¦ π§ β π ))} β π₯) |
32 | 16, 31 | eqsstrd 4020 |
. . . . . . . 8
β’ ((π₯ = (cardβran π) β§ (π΄ β On β§ π΅ β On) β§ (ran π β π΄ β§ βπ§ β π΄ βπ β ran π π§ β π )) β (cfβπ΄) β π₯) |
33 | 32 | 3expib 1123 |
. . . . . . 7
β’ (π₯ = (cardβran π) β (((π΄ β On β§ π΅ β On) β§ (ran π β π΄ β§ βπ§ β π΄ βπ β ran π π§ β π )) β (cfβπ΄) β π₯)) |
34 | | sseq2 4008 |
. . . . . . 7
β’ (π₯ = (cardβran π) β ((cfβπ΄) β π₯ β (cfβπ΄) β (cardβran π))) |
35 | 33, 34 | sylibd 238 |
. . . . . 6
β’ (π₯ = (cardβran π) β (((π΄ β On β§ π΅ β On) β§ (ran π β π΄ β§ βπ§ β π΄ βπ β ran π π§ β π )) β (cfβπ΄) β (cardβran π))) |
36 | 13, 35 | vtocle 3576 |
. . . . 5
β’ (((π΄ β On β§ π΅ β On) β§ (ran π β π΄ β§ βπ§ β π΄ βπ β ran π π§ β π )) β (cfβπ΄) β (cardβran π)) |
37 | 12, 36 | sylan2 594 |
. . . 4
β’ (((π΄ β On β§ π΅ β On) β§ (π:π΅βΆπ΄ β§ βπ§ β π΄ βπ€ β π΅ π§ β (πβπ€))) β (cfβπ΄) β (cardβran π)) |
38 | | cardidm 9951 |
. . . . . . 7
β’
(cardβ(cardβran π)) = (cardβran π) |
39 | | onss 7769 |
. . . . . . . . . . . . . 14
β’ (π΄ β On β π΄ β On) |
40 | 1, 39 | sylan9ssr 3996 |
. . . . . . . . . . . . 13
β’ ((π΄ β On β§ π:π΅βΆπ΄) β ran π β On) |
41 | 40 | 3adant2 1132 |
. . . . . . . . . . . 12
β’ ((π΄ β On β§ π΅ β On β§ π:π΅βΆπ΄) β ran π β On) |
42 | | onssnum 10032 |
. . . . . . . . . . . 12
β’ ((ran
π β V β§ ran π β On) β ran π β dom
card) |
43 | 18, 41, 42 | sylancr 588 |
. . . . . . . . . . 11
β’ ((π΄ β On β§ π΅ β On β§ π:π΅βΆπ΄) β ran π β dom card) |
44 | | cardid2 9945 |
. . . . . . . . . . 11
β’ (ran
π β dom card β
(cardβran π) β
ran π) |
45 | 43, 44 | syl 17 |
. . . . . . . . . 10
β’ ((π΄ β On β§ π΅ β On β§ π:π΅βΆπ΄) β (cardβran π) β ran π) |
46 | | onenon 9941 |
. . . . . . . . . . . . 13
β’ (π΅ β On β π΅ β dom
card) |
47 | | dffn4 6809 |
. . . . . . . . . . . . . 14
β’ (π Fn π΅ β π:π΅βontoβran π) |
48 | 3, 47 | sylib 217 |
. . . . . . . . . . . . 13
β’ (π:π΅βΆπ΄ β π:π΅βontoβran π) |
49 | | fodomnum 10049 |
. . . . . . . . . . . . 13
β’ (π΅ β dom card β (π:π΅βontoβran π β ran π βΌ π΅)) |
50 | 46, 48, 49 | syl2im 40 |
. . . . . . . . . . . 12
β’ (π΅ β On β (π:π΅βΆπ΄ β ran π βΌ π΅)) |
51 | 50 | imp 408 |
. . . . . . . . . . 11
β’ ((π΅ β On β§ π:π΅βΆπ΄) β ran π βΌ π΅) |
52 | 51 | 3adant1 1131 |
. . . . . . . . . 10
β’ ((π΄ β On β§ π΅ β On β§ π:π΅βΆπ΄) β ran π βΌ π΅) |
53 | | endomtr 9005 |
. . . . . . . . . 10
β’
(((cardβran π)
β ran π β§ ran
π βΌ π΅) β (cardβran π) βΌ π΅) |
54 | 45, 52, 53 | syl2anc 585 |
. . . . . . . . 9
β’ ((π΄ β On β§ π΅ β On β§ π:π΅βΆπ΄) β (cardβran π) βΌ π΅) |
55 | | cardon 9936 |
. . . . . . . . . . . 12
β’
(cardβran π)
β On |
56 | | onenon 9941 |
. . . . . . . . . . . 12
β’
((cardβran π)
β On β (cardβran π) β dom card) |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . . . 11
β’
(cardβran π)
β dom card |
58 | | carddom2 9969 |
. . . . . . . . . . 11
β’
(((cardβran π)
β dom card β§ π΅
β dom card) β ((cardβ(cardβran π)) β (cardβπ΅) β (cardβran π) βΌ π΅)) |
59 | 57, 46, 58 | sylancr 588 |
. . . . . . . . . 10
β’ (π΅ β On β
((cardβ(cardβran π)) β (cardβπ΅) β (cardβran π) βΌ π΅)) |
60 | 59 | 3ad2ant2 1135 |
. . . . . . . . 9
β’ ((π΄ β On β§ π΅ β On β§ π:π΅βΆπ΄) β ((cardβ(cardβran π)) β (cardβπ΅) β (cardβran π) βΌ π΅)) |
61 | 54, 60 | mpbird 257 |
. . . . . . . 8
β’ ((π΄ β On β§ π΅ β On β§ π:π΅βΆπ΄) β (cardβ(cardβran π)) β (cardβπ΅)) |
62 | | cardonle 9949 |
. . . . . . . . 9
β’ (π΅ β On β
(cardβπ΅) β
π΅) |
63 | 62 | 3ad2ant2 1135 |
. . . . . . . 8
β’ ((π΄ β On β§ π΅ β On β§ π:π΅βΆπ΄) β (cardβπ΅) β π΅) |
64 | 61, 63 | sstrd 3992 |
. . . . . . 7
β’ ((π΄ β On β§ π΅ β On β§ π:π΅βΆπ΄) β (cardβ(cardβran π)) β π΅) |
65 | 38, 64 | eqsstrrid 4031 |
. . . . . 6
β’ ((π΄ β On β§ π΅ β On β§ π:π΅βΆπ΄) β (cardβran π) β π΅) |
66 | 65 | 3expa 1119 |
. . . . 5
β’ (((π΄ β On β§ π΅ β On) β§ π:π΅βΆπ΄) β (cardβran π) β π΅) |
67 | 66 | adantrr 716 |
. . . 4
β’ (((π΄ β On β§ π΅ β On) β§ (π:π΅βΆπ΄ β§ βπ§ β π΄ βπ€ β π΅ π§ β (πβπ€))) β (cardβran π) β π΅) |
68 | 37, 67 | sstrd 3992 |
. . 3
β’ (((π΄ β On β§ π΅ β On) β§ (π:π΅βΆπ΄ β§ βπ§ β π΄ βπ€ β π΅ π§ β (πβπ€))) β (cfβπ΄) β π΅) |
69 | 68 | ex 414 |
. 2
β’ ((π΄ β On β§ π΅ β On) β ((π:π΅βΆπ΄ β§ βπ§ β π΄ βπ€ β π΅ π§ β (πβπ€)) β (cfβπ΄) β π΅)) |
70 | 69 | exlimdv 1937 |
1
β’ ((π΄ β On β§ π΅ β On) β (βπ(π:π΅βΆπ΄ β§ βπ§ β π΄ βπ€ β π΅ π§ β (πβπ€)) β (cfβπ΄) β π΅)) |