Step | Hyp | Ref
| Expression |
1 | | inawina 10684 |
. . . . . 6
β’ (π₯ β Inacc β π₯ β
Inaccw) |
2 | | winaon 10682 |
. . . . . 6
β’ (π₯ β Inaccw β
π₯ β
On) |
3 | 1, 2 | syl 17 |
. . . . 5
β’ (π₯ β Inacc β π₯ β On) |
4 | 3 | ssriv 3986 |
. . . 4
β’ Inacc
β On |
5 | | ssorduni 7765 |
. . . 4
β’ (Inacc
β On β Ord βͺ Inacc) |
6 | | ordsson 7769 |
. . . 4
β’ (Ord
βͺ Inacc β βͺ Inacc
β On) |
7 | 4, 5, 6 | mp2b 10 |
. . 3
β’ βͺ Inacc β On |
8 | | vex 3478 |
. . . . . . . 8
β’ π¦ β V |
9 | | grothtsk 10829 |
. . . . . . . 8
β’ βͺ Tarski = V |
10 | 8, 9 | eleqtrri 2832 |
. . . . . . 7
β’ π¦ β βͺ Tarski |
11 | | eluni2 4912 |
. . . . . . 7
β’ (π¦ β βͺ Tarski β βπ€ β Tarski π¦ β π€) |
12 | 10, 11 | mpbi 229 |
. . . . . 6
β’
βπ€ β
Tarski π¦ β π€ |
13 | | ne0i 4334 |
. . . . . . . . 9
β’ (π¦ β π€ β π€ β β
) |
14 | | tskcard 10775 |
. . . . . . . . 9
β’ ((π€ β Tarski β§ π€ β β
) β
(cardβπ€) β
Inacc) |
15 | 13, 14 | sylan2 593 |
. . . . . . . 8
β’ ((π€ β Tarski β§ π¦ β π€) β (cardβπ€) β Inacc) |
16 | | tsksdom 10750 |
. . . . . . . . . 10
β’ ((π€ β Tarski β§ π¦ β π€) β π¦ βΊ π€) |
17 | 16 | adantl 482 |
. . . . . . . . 9
β’ ((π¦ β On β§ (π€ β Tarski β§ π¦ β π€)) β π¦ βΊ π€) |
18 | | tskwe2 10767 |
. . . . . . . . . . 11
β’ (π€ β Tarski β π€ β dom
card) |
19 | 18 | adantr 481 |
. . . . . . . . . 10
β’ ((π€ β Tarski β§ π¦ β π€) β π€ β dom card) |
20 | | cardsdomel 9968 |
. . . . . . . . . 10
β’ ((π¦ β On β§ π€ β dom card) β (π¦ βΊ π€ β π¦ β (cardβπ€))) |
21 | 19, 20 | sylan2 593 |
. . . . . . . . 9
β’ ((π¦ β On β§ (π€ β Tarski β§ π¦ β π€)) β (π¦ βΊ π€ β π¦ β (cardβπ€))) |
22 | 17, 21 | mpbid 231 |
. . . . . . . 8
β’ ((π¦ β On β§ (π€ β Tarski β§ π¦ β π€)) β π¦ β (cardβπ€)) |
23 | | eleq2 2822 |
. . . . . . . . 9
β’ (π§ = (cardβπ€) β (π¦ β π§ β π¦ β (cardβπ€))) |
24 | 23 | rspcev 3612 |
. . . . . . . 8
β’
(((cardβπ€)
β Inacc β§ π¦ β
(cardβπ€)) β
βπ§ β Inacc π¦ β π§) |
25 | 15, 22, 24 | syl2an2 684 |
. . . . . . 7
β’ ((π¦ β On β§ (π€ β Tarski β§ π¦ β π€)) β βπ§ β Inacc π¦ β π§) |
26 | 25 | rexlimdvaa 3156 |
. . . . . 6
β’ (π¦ β On β (βπ€ β Tarski π¦ β π€ β βπ§ β Inacc π¦ β π§)) |
27 | 12, 26 | mpi 20 |
. . . . 5
β’ (π¦ β On β βπ§ β Inacc π¦ β π§) |
28 | | eluni2 4912 |
. . . . 5
β’ (π¦ β βͺ Inacc β βπ§ β Inacc π¦ β π§) |
29 | 27, 28 | sylibr 233 |
. . . 4
β’ (π¦ β On β π¦ β βͺ Inacc) |
30 | 29 | ssriv 3986 |
. . 3
β’ On
β βͺ Inacc |
31 | 7, 30 | eqssi 3998 |
. 2
β’ βͺ Inacc = On |
32 | | ssonprc 7774 |
. . 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 |