Step | Hyp | Ref
| Expression |
1 | | dfac3 10116 |
. . 3
β’
(CHOICE β βπβπβπ β π (π β β
β (πβπ) β π)) |
2 | | raleq 3323 |
. . . . . 6
β’ (π = π₯ β (βπ β π (π β β
β (πβπ) β π) β βπ β π₯ (π β β
β (πβπ) β π))) |
3 | 2 | exbidv 1925 |
. . . . 5
β’ (π = π₯ β (βπβπ β π (π β β
β (πβπ) β π) β βπβπ β π₯ (π β β
β (πβπ) β π))) |
4 | 3 | cbvalvw 2040 |
. . . 4
β’
(βπβπβπ β π (π β β
β (πβπ) β π) β βπ₯βπβπ β π₯ (π β β
β (πβπ) β π)) |
5 | | neeq1 3004 |
. . . . . . . . . 10
β’ (π = π§ β (π β β
β π§ β β
)) |
6 | | fveq2 6892 |
. . . . . . . . . . 11
β’ (π = π§ β (πβπ) = (πβπ§)) |
7 | | id 22 |
. . . . . . . . . . 11
β’ (π = π§ β π = π§) |
8 | 6, 7 | eleq12d 2828 |
. . . . . . . . . 10
β’ (π = π§ β ((πβπ) β π β (πβπ§) β π§)) |
9 | 5, 8 | imbi12d 345 |
. . . . . . . . 9
β’ (π = π§ β ((π β β
β (πβπ) β π) β (π§ β β
β (πβπ§) β π§))) |
10 | 9 | cbvralvw 3235 |
. . . . . . . 8
β’
(βπ β
π₯ (π β β
β (πβπ) β π) β βπ§ β π₯ (π§ β β
β (πβπ§) β π§)) |
11 | | fveq2 6892 |
. . . . . . . . . . . . . . 15
β’ (π = π§ β (πβπ) = (πβπ§)) |
12 | 11 | sneqd 4641 |
. . . . . . . . . . . . . 14
β’ (π = π§ β {(πβπ)} = {(πβπ§)}) |
13 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’ (π β π₯ β¦ {(πβπ)}) = (π β π₯ β¦ {(πβπ)}) |
14 | | snex 5432 |
. . . . . . . . . . . . . 14
β’ {(πβπ§)} β V |
15 | 12, 13, 14 | fvmpt 6999 |
. . . . . . . . . . . . 13
β’ (π§ β π₯ β ((π β π₯ β¦ {(πβπ)})βπ§) = {(πβπ§)}) |
16 | 15 | 3ad2ant1 1134 |
. . . . . . . . . . . 12
β’ ((π§ β π₯ β§ π§ β β
β§ (πβπ§) β π§) β ((π β π₯ β¦ {(πβπ)})βπ§) = {(πβπ§)}) |
17 | | simp3 1139 |
. . . . . . . . . . . . . . . 16
β’ ((π§ β π₯ β§ π§ β β
β§ (πβπ§) β π§) β (πβπ§) β π§) |
18 | 17 | snssd 4813 |
. . . . . . . . . . . . . . 15
β’ ((π§ β π₯ β§ π§ β β
β§ (πβπ§) β π§) β {(πβπ§)} β π§) |
19 | 14 | elpw 4607 |
. . . . . . . . . . . . . . 15
β’ ({(πβπ§)} β π« π§ β {(πβπ§)} β π§) |
20 | 18, 19 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ ((π§ β π₯ β§ π§ β β
β§ (πβπ§) β π§) β {(πβπ§)} β π« π§) |
21 | | snfi 9044 |
. . . . . . . . . . . . . . 15
β’ {(πβπ§)} β Fin |
22 | 21 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π§ β π₯ β§ π§ β β
β§ (πβπ§) β π§) β {(πβπ§)} β Fin) |
23 | 20, 22 | elind 4195 |
. . . . . . . . . . . . 13
β’ ((π§ β π₯ β§ π§ β β
β§ (πβπ§) β π§) β {(πβπ§)} β (π« π§ β© Fin)) |
24 | | fvex 6905 |
. . . . . . . . . . . . . . 15
β’ (πβπ§) β V |
25 | 24 | snnz 4781 |
. . . . . . . . . . . . . 14
β’ {(πβπ§)} β β
|
26 | 25 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π§ β π₯ β§ π§ β β
β§ (πβπ§) β π§) β {(πβπ§)} β β
) |
27 | | eldifsn 4791 |
. . . . . . . . . . . . 13
β’ ({(πβπ§)} β ((π« π§ β© Fin) β {β
}) β
({(πβπ§)} β (π« π§ β© Fin) β§ {(πβπ§)} β β
)) |
28 | 23, 26, 27 | sylanbrc 584 |
. . . . . . . . . . . 12
β’ ((π§ β π₯ β§ π§ β β
β§ (πβπ§) β π§) β {(πβπ§)} β ((π« π§ β© Fin) β
{β
})) |
29 | 16, 28 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ ((π§ β π₯ β§ π§ β β
β§ (πβπ§) β π§) β ((π β π₯ β¦ {(πβπ)})βπ§) β ((π« π§ β© Fin) β
{β
})) |
30 | 29 | 3exp 1120 |
. . . . . . . . . 10
β’ (π§ β π₯ β (π§ β β
β ((πβπ§) β π§ β ((π β π₯ β¦ {(πβπ)})βπ§) β ((π« π§ β© Fin) β
{β
})))) |
31 | 30 | a2d 29 |
. . . . . . . . 9
β’ (π§ β π₯ β ((π§ β β
β (πβπ§) β π§) β (π§ β β
β ((π β π₯ β¦ {(πβπ)})βπ§) β ((π« π§ β© Fin) β
{β
})))) |
32 | 31 | ralimia 3081 |
. . . . . . . 8
β’
(βπ§ β
π₯ (π§ β β
β (πβπ§) β π§) β βπ§ β π₯ (π§ β β
β ((π β π₯ β¦ {(πβπ)})βπ§) β ((π« π§ β© Fin) β
{β
}))) |
33 | 10, 32 | sylbi 216 |
. . . . . . 7
β’
(βπ β
π₯ (π β β
β (πβπ) β π) β βπ§ β π₯ (π§ β β
β ((π β π₯ β¦ {(πβπ)})βπ§) β ((π« π§ β© Fin) β
{β
}))) |
34 | | vex 3479 |
. . . . . . . . 9
β’ π₯ β V |
35 | 34 | mptex 7225 |
. . . . . . . 8
β’ (π β π₯ β¦ {(πβπ)}) β V |
36 | | fveq1 6891 |
. . . . . . . . . . 11
β’ (π = (π β π₯ β¦ {(πβπ)}) β (πβπ§) = ((π β π₯ β¦ {(πβπ)})βπ§)) |
37 | 36 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π = (π β π₯ β¦ {(πβπ)}) β ((πβπ§) β ((π« π§ β© Fin) β {β
}) β ((π β π₯ β¦ {(πβπ)})βπ§) β ((π« π§ β© Fin) β
{β
}))) |
38 | 37 | imbi2d 341 |
. . . . . . . . 9
β’ (π = (π β π₯ β¦ {(πβπ)}) β ((π§ β β
β (πβπ§) β ((π« π§ β© Fin) β {β
})) β (π§ β β
β ((π β π₯ β¦ {(πβπ)})βπ§) β ((π« π§ β© Fin) β
{β
})))) |
39 | 38 | ralbidv 3178 |
. . . . . . . 8
β’ (π = (π β π₯ β¦ {(πβπ)}) β (βπ§ β π₯ (π§ β β
β (πβπ§) β ((π« π§ β© Fin) β {β
})) β
βπ§ β π₯ (π§ β β
β ((π β π₯ β¦ {(πβπ)})βπ§) β ((π« π§ β© Fin) β
{β
})))) |
40 | 35, 39 | spcev 3597 |
. . . . . . 7
β’
(βπ§ β
π₯ (π§ β β
β ((π β π₯ β¦ {(πβπ)})βπ§) β ((π« π§ β© Fin) β {β
})) β
βπβπ§ β π₯ (π§ β β
β (πβπ§) β ((π« π§ β© Fin) β
{β
}))) |
41 | 33, 40 | syl 17 |
. . . . . 6
β’
(βπ β
π₯ (π β β
β (πβπ) β π) β βπβπ§ β π₯ (π§ β β
β (πβπ§) β ((π« π§ β© Fin) β
{β
}))) |
42 | 41 | exlimiv 1934 |
. . . . 5
β’
(βπβπ β π₯ (π β β
β (πβπ) β π) β βπβπ§ β π₯ (π§ β β
β (πβπ§) β ((π« π§ β© Fin) β
{β
}))) |
43 | 42 | alimi 1814 |
. . . 4
β’
(βπ₯βπβπ β π₯ (π β β
β (πβπ) β π) β βπ₯βπβπ§ β π₯ (π§ β β
β (πβπ§) β ((π« π§ β© Fin) β
{β
}))) |
44 | 4, 43 | sylbi 216 |
. . 3
β’
(βπβπβπ β π (π β β
β (πβπ) β π) β βπ₯βπβπ§ β π₯ (π§ β β
β (πβπ§) β ((π« π§ β© Fin) β
{β
}))) |
45 | 1, 44 | sylbi 216 |
. 2
β’
(CHOICE β βπ₯βπβπ§ β π₯ (π§ β β
β (πβπ§) β ((π« π§ β© Fin) β
{β
}))) |
46 | | fvex 6905 |
. . . . . . 7
β’
(π
1β(rankβπ)) β V |
47 | 46 | pwex 5379 |
. . . . . 6
β’ π«
(π
1β(rankβπ)) β V |
48 | | raleq 3323 |
. . . . . . 7
β’ (π₯ = π«
(π
1β(rankβπ)) β (βπ§ β π₯ (π§ β β
β (πβπ§) β ((π« π§ β© Fin) β {β
})) β
βπ§ β π«
(π
1β(rankβπ))(π§ β β
β (πβπ§) β ((π« π§ β© Fin) β
{β
})))) |
49 | 48 | exbidv 1925 |
. . . . . 6
β’ (π₯ = π«
(π
1β(rankβπ)) β (βπβπ§ β π₯ (π§ β β
β (πβπ§) β ((π« π§ β© Fin) β {β
})) β
βπβπ§ β π«
(π
1β(rankβπ))(π§ β β
β (πβπ§) β ((π« π§ β© Fin) β
{β
})))) |
50 | 47, 49 | spcv 3596 |
. . . . 5
β’
(βπ₯βπβπ§ β π₯ (π§ β β
β (πβπ§) β ((π« π§ β© Fin) β {β
})) β
βπβπ§ β π«
(π
1β(rankβπ))(π§ β β
β (πβπ§) β ((π« π§ β© Fin) β
{β
}))) |
51 | | rankon 9790 |
. . . . . . . 8
β’
(rankβπ)
β On |
52 | 51 | a1i 11 |
. . . . . . 7
β’
(βπ§ β
π« (π
1β(rankβπ))(π§ β β
β (πβπ§) β ((π« π§ β© Fin) β {β
})) β
(rankβπ) β
On) |
53 | | id 22 |
. . . . . . 7
β’
(βπ§ β
π« (π
1β(rankβπ))(π§ β β
β (πβπ§) β ((π« π§ β© Fin) β {β
})) β
βπ§ β π«
(π
1β(rankβπ))(π§ β β
β (πβπ§) β ((π« π§ β© Fin) β
{β
}))) |
54 | 52, 53 | aomclem8 41803 |
. . . . . 6
β’
(βπ§ β
π« (π
1β(rankβπ))(π§ β β
β (πβπ§) β ((π« π§ β© Fin) β {β
})) β
βπ π We
(π
1β(rankβπ))) |
55 | 54 | exlimiv 1934 |
. . . . 5
β’
(βπβπ§ β π«
(π
1β(rankβπ))(π§ β β
β (πβπ§) β ((π« π§ β© Fin) β {β
})) β
βπ π We
(π
1β(rankβπ))) |
56 | | vex 3479 |
. . . . . 6
β’ π β V |
57 | | r1rankid 9854 |
. . . . . 6
β’ (π β V β π β
(π
1β(rankβπ))) |
58 | | wess 5664 |
. . . . . . 7
β’ (π β
(π
1β(rankβπ)) β (π We
(π
1β(rankβπ)) β π We π)) |
59 | 58 | eximdv 1921 |
. . . . . 6
β’ (π β
(π
1β(rankβπ)) β (βπ π We
(π
1β(rankβπ)) β βπ π We π)) |
60 | 56, 57, 59 | mp2b 10 |
. . . . 5
β’
(βπ π We
(π
1β(rankβπ)) β βπ π We π) |
61 | 50, 55, 60 | 3syl 18 |
. . . 4
β’
(βπ₯βπβπ§ β π₯ (π§ β β
β (πβπ§) β ((π« π§ β© Fin) β {β
})) β
βπ π We π) |
62 | 61 | alrimiv 1931 |
. . 3
β’
(βπ₯βπβπ§ β π₯ (π§ β β
β (πβπ§) β ((π« π§ β© Fin) β {β
})) β
βπβπ π We π) |
63 | | dfac8 10130 |
. . 3
β’
(CHOICE β βπβπ π We π) |
64 | 62, 63 | sylibr 233 |
. 2
β’
(βπ₯βπβπ§ β π₯ (π§ β β
β (πβπ§) β ((π« π§ β© Fin) β {β
})) β
CHOICE) |
65 | 45, 64 | impbii 208 |
1
β’
(CHOICE β βπ₯βπβπ§ β π₯ (π§ β β
β (πβπ§) β ((π« π§ β© Fin) β
{β
}))) |