Step | Hyp | Ref
| Expression |
1 | | eqcom 2744 |
. 2
β’
((cardβπ΄) =
π΄ β π΄ = (cardβπ΄)) |
2 | | mptrel 5782 |
. . . . 5
β’ Rel
(π₯ β V β¦ β© {π¦
β On β£ π¦ β
π₯}) |
3 | | df-card 9876 |
. . . . . 6
β’ card =
(π₯ β V β¦ β© {π¦
β On β£ π¦ β
π₯}) |
4 | 3 | releqi 5734 |
. . . . 5
β’ (Rel card
β Rel (π₯ β V
β¦ β© {π¦ β On β£ π¦ β π₯})) |
5 | 2, 4 | mpbir 230 |
. . . 4
β’ Rel
card |
6 | | relelrnb 5903 |
. . . 4
β’ (Rel card
β (π΄ β ran card
β βπ₯ π₯cardπ΄)) |
7 | 5, 6 | ax-mp 5 |
. . 3
β’ (π΄ β ran card β
βπ₯ π₯cardπ΄) |
8 | 3 | funmpt2 6541 |
. . . . . . 7
β’ Fun
card |
9 | | funbrfv 6894 |
. . . . . . 7
β’ (Fun card
β (π₯cardπ΄ β (cardβπ₯) = π΄)) |
10 | 8, 9 | ax-mp 5 |
. . . . . 6
β’ (π₯cardπ΄ β (cardβπ₯) = π΄) |
11 | 10 | eqcomd 2743 |
. . . . 5
β’ (π₯cardπ΄ β π΄ = (cardβπ₯)) |
12 | 11 | eximi 1838 |
. . . 4
β’
(βπ₯ π₯cardπ΄ β βπ₯ π΄ = (cardβπ₯)) |
13 | | cardidm 9896 |
. . . . . . 7
β’
(cardβ(cardβπ₯)) = (cardβπ₯) |
14 | | fveq2 6843 |
. . . . . . 7
β’ (π΄ = (cardβπ₯) β (cardβπ΄) =
(cardβ(cardβπ₯))) |
15 | | id 22 |
. . . . . . 7
β’ (π΄ = (cardβπ₯) β π΄ = (cardβπ₯)) |
16 | 13, 14, 15 | 3eqtr4a 2803 |
. . . . . 6
β’ (π΄ = (cardβπ₯) β (cardβπ΄) = π΄) |
17 | 16 | exlimiv 1934 |
. . . . 5
β’
(βπ₯ π΄ = (cardβπ₯) β (cardβπ΄) = π΄) |
18 | 1 | biimpi 215 |
. . . . . . . . . . 11
β’
((cardβπ΄) =
π΄ β π΄ = (cardβπ΄)) |
19 | | cardon 9881 |
. . . . . . . . . . 11
β’
(cardβπ΄)
β On |
20 | 18, 19 | eqeltrdi 2846 |
. . . . . . . . . 10
β’
((cardβπ΄) =
π΄ β π΄ β On) |
21 | | onenon 9886 |
. . . . . . . . . 10
β’ (π΄ β On β π΄ β dom
card) |
22 | 20, 21 | syl 17 |
. . . . . . . . 9
β’
((cardβπ΄) =
π΄ β π΄ β dom card) |
23 | | funfvbrb 7002 |
. . . . . . . . . 10
β’ (Fun card
β (π΄ β dom card
β π΄card(cardβπ΄))) |
24 | 23 | biimpd 228 |
. . . . . . . . 9
β’ (Fun card
β (π΄ β dom card
β π΄card(cardβπ΄))) |
25 | 8, 22, 24 | mpsyl 68 |
. . . . . . . 8
β’
((cardβπ΄) =
π΄ β π΄card(cardβπ΄)) |
26 | | id 22 |
. . . . . . . 8
β’
((cardβπ΄) =
π΄ β (cardβπ΄) = π΄) |
27 | 25, 26 | breqtrd 5132 |
. . . . . . 7
β’
((cardβπ΄) =
π΄ β π΄cardπ΄) |
28 | | id 22 |
. . . . . . . . . 10
β’ (π΄ = (cardβπ΄) β π΄ = (cardβπ΄)) |
29 | 28, 19 | eqeltrdi 2846 |
. . . . . . . . 9
β’ (π΄ = (cardβπ΄) β π΄ β On) |
30 | 29 | eqcoms 2745 |
. . . . . . . 8
β’
((cardβπ΄) =
π΄ β π΄ β On) |
31 | | sbcbr1g 5163 |
. . . . . . . . 9
β’ (π΄ β On β ([π΄ / π₯]π₯cardπ΄ β β¦π΄ / π₯β¦π₯cardπ΄)) |
32 | | csbvarg 4392 |
. . . . . . . . . 10
β’ (π΄ β On β
β¦π΄ / π₯β¦π₯ = π΄) |
33 | 32 | breq1d 5116 |
. . . . . . . . 9
β’ (π΄ β On β
(β¦π΄ / π₯β¦π₯cardπ΄ β π΄cardπ΄)) |
34 | 31, 33 | bitrd 279 |
. . . . . . . 8
β’ (π΄ β On β ([π΄ / π₯]π₯cardπ΄ β π΄cardπ΄)) |
35 | 30, 34 | syl 17 |
. . . . . . 7
β’
((cardβπ΄) =
π΄ β ([π΄ / π₯]π₯cardπ΄ β π΄cardπ΄)) |
36 | 27, 35 | mpbird 257 |
. . . . . 6
β’
((cardβπ΄) =
π΄ β [π΄ / π₯]π₯cardπ΄) |
37 | 36 | spesbcd 3840 |
. . . . 5
β’
((cardβπ΄) =
π΄ β βπ₯ π₯cardπ΄) |
38 | 17, 37 | syl 17 |
. . . 4
β’
(βπ₯ π΄ = (cardβπ₯) β βπ₯ π₯cardπ΄) |
39 | 12, 38 | impbii 208 |
. . 3
β’
(βπ₯ π₯cardπ΄ β βπ₯ π΄ = (cardβπ₯)) |
40 | | oncard 9897 |
. . 3
β’
(βπ₯ π΄ = (cardβπ₯) β π΄ = (cardβπ΄)) |
41 | 7, 39, 40 | 3bitrri 298 |
. 2
β’ (π΄ = (cardβπ΄) β π΄ β ran card) |
42 | 1, 41 | bitri 275 |
1
β’
((cardβπ΄) =
π΄ β π΄ β ran card) |