Step | Hyp | Ref
| Expression |
1 | | inawina 10634 |
. . . . . 6
β’ (π₯ β Inacc β π₯ β
Inaccw) |
2 | | winaon 10632 |
. . . . . 6
β’ (π₯ β Inaccw β
π₯ β
On) |
3 | 1, 2 | syl 17 |
. . . . 5
β’ (π₯ β Inacc β π₯ β On) |
4 | 3 | ssriv 3952 |
. . . 4
β’ Inacc
β On |
5 | | ssorduni 7717 |
. . . 4
β’ (Inacc
β On β Ord βͺ Inacc) |
6 | | ordsson 7721 |
. . . 4
β’ (Ord
βͺ Inacc β βͺ Inacc
β On) |
7 | 4, 5, 6 | mp2b 10 |
. . 3
β’ βͺ Inacc β On |
8 | | vex 3451 |
. . . . . . . 8
β’ π¦ β V |
9 | | grothtsk 10779 |
. . . . . . . 8
β’ βͺ Tarski = V |
10 | 8, 9 | eleqtrri 2833 |
. . . . . . 7
β’ π¦ β βͺ Tarski |
11 | | eluni2 4873 |
. . . . . . 7
β’ (π¦ β βͺ Tarski β βπ€ β Tarski π¦ β π€) |
12 | 10, 11 | mpbi 229 |
. . . . . 6
β’
βπ€ β
Tarski π¦ β π€ |
13 | | ne0i 4298 |
. . . . . . . . 9
β’ (π¦ β π€ β π€ β β
) |
14 | | tskcard 10725 |
. . . . . . . . 9
β’ ((π€ β Tarski β§ π€ β β
) β
(cardβπ€) β
Inacc) |
15 | 13, 14 | sylan2 594 |
. . . . . . . 8
β’ ((π€ β Tarski β§ π¦ β π€) β (cardβπ€) β Inacc) |
16 | | tsksdom 10700 |
. . . . . . . . . 10
β’ ((π€ β Tarski β§ π¦ β π€) β π¦ βΊ π€) |
17 | 16 | adantl 483 |
. . . . . . . . 9
β’ ((π¦ β On β§ (π€ β Tarski β§ π¦ β π€)) β π¦ βΊ π€) |
18 | | tskwe2 10717 |
. . . . . . . . . . 11
β’ (π€ β Tarski β π€ β dom
card) |
19 | 18 | adantr 482 |
. . . . . . . . . 10
β’ ((π€ β Tarski β§ π¦ β π€) β π€ β dom card) |
20 | | cardsdomel 9918 |
. . . . . . . . . 10
β’ ((π¦ β On β§ π€ β dom card) β (π¦ βΊ π€ β π¦ β (cardβπ€))) |
21 | 19, 20 | sylan2 594 |
. . . . . . . . 9
β’ ((π¦ β On β§ (π€ β Tarski β§ π¦ β π€)) β (π¦ βΊ π€ β π¦ β (cardβπ€))) |
22 | 17, 21 | mpbid 231 |
. . . . . . . 8
β’ ((π¦ β On β§ (π€ β Tarski β§ π¦ β π€)) β π¦ β (cardβπ€)) |
23 | | eleq2 2823 |
. . . . . . . . 9
β’ (π§ = (cardβπ€) β (π¦ β π§ β π¦ β (cardβπ€))) |
24 | 23 | rspcev 3583 |
. . . . . . . 8
β’
(((cardβπ€)
β Inacc β§ π¦ β
(cardβπ€)) β
βπ§ β Inacc π¦ β π§) |
25 | 15, 22, 24 | syl2an2 685 |
. . . . . . 7
β’ ((π¦ β On β§ (π€ β Tarski β§ π¦ β π€)) β βπ§ β Inacc π¦ β π§) |
26 | 25 | rexlimdvaa 3150 |
. . . . . 6
β’ (π¦ β On β (βπ€ β Tarski π¦ β π€ β βπ§ β Inacc π¦ β π§)) |
27 | 12, 26 | mpi 20 |
. . . . 5
β’ (π¦ β On β βπ§ β Inacc π¦ β π§) |
28 | | eluni2 4873 |
. . . . 5
β’ (π¦ β βͺ Inacc β βπ§ β Inacc π¦ β π§) |
29 | 27, 28 | sylibr 233 |
. . . 4
β’ (π¦ β On β π¦ β βͺ Inacc) |
30 | 29 | ssriv 3952 |
. . 3
β’ On
β βͺ Inacc |
31 | 7, 30 | eqssi 3964 |
. 2
β’ βͺ Inacc = On |
32 | | ssonprc 7726 |
. . 3
β’ (Inacc
β On β (Inacc β V β βͺ Inacc =
On)) |
33 | 4, 32 | ax-mp 5 |
. 2
β’ (Inacc
β V β βͺ Inacc = On) |
34 | 31, 33 | mpbir 230 |
1
β’ Inacc
β V |