Step | Hyp | Ref
| Expression |
1 | | unieq 4920 |
. . . . 5
β’ (π₯ = π΄ β βͺ π₯ = βͺ
π΄) |
2 | 1 | fveq2d 6896 |
. . . 4
β’ (π₯ = π΄ β (rankββͺ π₯) =
(rankββͺ π΄)) |
3 | | fveq2 6892 |
. . . . 5
β’ (π₯ = π΄ β (rankβπ₯) = (rankβπ΄)) |
4 | 3 | unieqd 4923 |
. . . 4
β’ (π₯ = π΄ β βͺ
(rankβπ₯) = βͺ (rankβπ΄)) |
5 | 2, 4 | eqeq12d 2749 |
. . 3
β’ (π₯ = π΄ β ((rankββͺ π₯) =
βͺ (rankβπ₯) β (rankββͺ π΄) =
βͺ (rankβπ΄))) |
6 | | vex 3479 |
. . . . . . 7
β’ π₯ β V |
7 | 6 | rankuni2 9850 |
. . . . . 6
β’
(rankββͺ π₯) = βͺ π§ β π₯ (rankβπ§) |
8 | | fvex 6905 |
. . . . . . 7
β’
(rankβπ§)
β V |
9 | 8 | dfiun2 5037 |
. . . . . 6
β’ βͺ π§ β π₯ (rankβπ§) = βͺ {π¦ β£ βπ§ β π₯ π¦ = (rankβπ§)} |
10 | 7, 9 | eqtri 2761 |
. . . . 5
β’
(rankββͺ π₯) = βͺ {π¦ β£ βπ§ β π₯ π¦ = (rankβπ§)} |
11 | | df-rex 3072 |
. . . . . . . 8
β’
(βπ§ β
π₯ π¦ = (rankβπ§) β βπ§(π§ β π₯ β§ π¦ = (rankβπ§))) |
12 | 6 | rankel 9834 |
. . . . . . . . . . 11
β’ (π§ β π₯ β (rankβπ§) β (rankβπ₯)) |
13 | 12 | anim1i 616 |
. . . . . . . . . 10
β’ ((π§ β π₯ β§ π¦ = (rankβπ§)) β ((rankβπ§) β (rankβπ₯) β§ π¦ = (rankβπ§))) |
14 | 13 | eximi 1838 |
. . . . . . . . 9
β’
(βπ§(π§ β π₯ β§ π¦ = (rankβπ§)) β βπ§((rankβπ§) β (rankβπ₯) β§ π¦ = (rankβπ§))) |
15 | | 19.42v 1958 |
. . . . . . . . . 10
β’
(βπ§(π¦ β (rankβπ₯) β§ π¦ = (rankβπ§)) β (π¦ β (rankβπ₯) β§ βπ§ π¦ = (rankβπ§))) |
16 | | eleq1 2822 |
. . . . . . . . . . . 12
β’ (π¦ = (rankβπ§) β (π¦ β (rankβπ₯) β (rankβπ§) β (rankβπ₯))) |
17 | 16 | pm5.32ri 577 |
. . . . . . . . . . 11
β’ ((π¦ β (rankβπ₯) β§ π¦ = (rankβπ§)) β ((rankβπ§) β (rankβπ₯) β§ π¦ = (rankβπ§))) |
18 | 17 | exbii 1851 |
. . . . . . . . . 10
β’
(βπ§(π¦ β (rankβπ₯) β§ π¦ = (rankβπ§)) β βπ§((rankβπ§) β (rankβπ₯) β§ π¦ = (rankβπ§))) |
19 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π¦ β (rankβπ₯) β§ βπ§ π¦ = (rankβπ§)) β π¦ β (rankβπ₯)) |
20 | | rankon 9790 |
. . . . . . . . . . . . . . . . 17
β’
(rankβπ₯)
β On |
21 | 20 | oneli 6479 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β (rankβπ₯) β π¦ β On) |
22 | | r1fnon 9762 |
. . . . . . . . . . . . . . . . 17
β’
π
1 Fn On |
23 | | fndm 6653 |
. . . . . . . . . . . . . . . . 17
β’
(π
1 Fn On β dom π
1 =
On) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ dom
π
1 = On |
25 | 21, 24 | eleqtrrdi 2845 |
. . . . . . . . . . . . . . 15
β’ (π¦ β (rankβπ₯) β π¦ β dom
π
1) |
26 | | rankr1id 9857 |
. . . . . . . . . . . . . . 15
β’ (π¦ β dom
π
1 β (rankβ(π
1βπ¦)) = π¦) |
27 | 25, 26 | sylib 217 |
. . . . . . . . . . . . . 14
β’ (π¦ β (rankβπ₯) β
(rankβ(π
1βπ¦)) = π¦) |
28 | 27 | eqcomd 2739 |
. . . . . . . . . . . . 13
β’ (π¦ β (rankβπ₯) β π¦ =
(rankβ(π
1βπ¦))) |
29 | | fvex 6905 |
. . . . . . . . . . . . . 14
β’
(π
1βπ¦) β V |
30 | | fveq2 6892 |
. . . . . . . . . . . . . . 15
β’ (π§ =
(π
1βπ¦) β (rankβπ§) =
(rankβ(π
1βπ¦))) |
31 | 30 | eqeq2d 2744 |
. . . . . . . . . . . . . 14
β’ (π§ =
(π
1βπ¦) β (π¦ = (rankβπ§) β π¦ =
(rankβ(π
1βπ¦)))) |
32 | 29, 31 | spcev 3597 |
. . . . . . . . . . . . 13
β’ (π¦ =
(rankβ(π
1βπ¦)) β βπ§ π¦ = (rankβπ§)) |
33 | 28, 32 | syl 17 |
. . . . . . . . . . . 12
β’ (π¦ β (rankβπ₯) β βπ§ π¦ = (rankβπ§)) |
34 | 33 | ancli 550 |
. . . . . . . . . . 11
β’ (π¦ β (rankβπ₯) β (π¦ β (rankβπ₯) β§ βπ§ π¦ = (rankβπ§))) |
35 | 19, 34 | impbii 208 |
. . . . . . . . . 10
β’ ((π¦ β (rankβπ₯) β§ βπ§ π¦ = (rankβπ§)) β π¦ β (rankβπ₯)) |
36 | 15, 18, 35 | 3bitr3i 301 |
. . . . . . . . 9
β’
(βπ§((rankβπ§) β (rankβπ₯) β§ π¦ = (rankβπ§)) β π¦ β (rankβπ₯)) |
37 | 14, 36 | sylib 217 |
. . . . . . . 8
β’
(βπ§(π§ β π₯ β§ π¦ = (rankβπ§)) β π¦ β (rankβπ₯)) |
38 | 11, 37 | sylbi 216 |
. . . . . . 7
β’
(βπ§ β
π₯ π¦ = (rankβπ§) β π¦ β (rankβπ₯)) |
39 | 38 | abssi 4068 |
. . . . . 6
β’ {π¦ β£ βπ§ β π₯ π¦ = (rankβπ§)} β (rankβπ₯) |
40 | 39 | unissi 4918 |
. . . . 5
β’ βͺ {π¦
β£ βπ§ β
π₯ π¦ = (rankβπ§)} β βͺ
(rankβπ₯) |
41 | 10, 40 | eqsstri 4017 |
. . . 4
β’
(rankββͺ π₯) β βͺ
(rankβπ₯) |
42 | | pwuni 4950 |
. . . . . . . 8
β’ π₯ β π« βͺ π₯ |
43 | | vuniex 7729 |
. . . . . . . . . 10
β’ βͺ π₯
β V |
44 | 43 | pwex 5379 |
. . . . . . . . 9
β’ π«
βͺ π₯ β V |
45 | 44 | rankss 9844 |
. . . . . . . 8
β’ (π₯ β π« βͺ π₯
β (rankβπ₯)
β (rankβπ« βͺ π₯)) |
46 | 42, 45 | ax-mp 5 |
. . . . . . 7
β’
(rankβπ₯)
β (rankβπ« βͺ π₯) |
47 | 43 | rankpw 9838 |
. . . . . . 7
β’
(rankβπ« βͺ π₯) = suc (rankββͺ π₯) |
48 | 46, 47 | sseqtri 4019 |
. . . . . 6
β’
(rankβπ₯)
β suc (rankββͺ π₯) |
49 | 48 | unissi 4918 |
. . . . 5
β’ βͺ (rankβπ₯) β βͺ suc
(rankββͺ π₯) |
50 | | rankon 9790 |
. . . . . 6
β’
(rankββͺ π₯) β On |
51 | 50 | onunisuci 6485 |
. . . . 5
β’ βͺ suc (rankββͺ π₯) = (rankββͺ π₯) |
52 | 49, 51 | sseqtri 4019 |
. . . 4
β’ βͺ (rankβπ₯) β (rankββͺ π₯) |
53 | 41, 52 | eqssi 3999 |
. . 3
β’
(rankββͺ π₯) = βͺ
(rankβπ₯) |
54 | 5, 53 | vtoclg 3557 |
. 2
β’ (π΄ β V β
(rankββͺ π΄) = βͺ
(rankβπ΄)) |
55 | | uniexb 7751 |
. . . . 5
β’ (π΄ β V β βͺ π΄
β V) |
56 | | fvprc 6884 |
. . . . 5
β’ (Β¬
βͺ π΄ β V β (rankββͺ π΄) =
β
) |
57 | 55, 56 | sylnbi 330 |
. . . 4
β’ (Β¬
π΄ β V β
(rankββͺ π΄) = β
) |
58 | | uni0 4940 |
. . . 4
β’ βͺ β
= β
|
59 | 57, 58 | eqtr4di 2791 |
. . 3
β’ (Β¬
π΄ β V β
(rankββͺ π΄) = βͺ
β
) |
60 | | fvprc 6884 |
. . . 4
β’ (Β¬
π΄ β V β
(rankβπ΄) =
β
) |
61 | 60 | unieqd 4923 |
. . 3
β’ (Β¬
π΄ β V β βͺ (rankβπ΄) = βͺ
β
) |
62 | 59, 61 | eqtr4d 2776 |
. 2
β’ (Β¬
π΄ β V β
(rankββͺ π΄) = βͺ
(rankβπ΄)) |
63 | 54, 62 | pm2.61i 182 |
1
β’
(rankββͺ π΄) = βͺ
(rankβπ΄) |