Step |
Hyp |
Ref |
Expression |
1 |
|
inawina |
⊢ ( 𝑥 ∈ Inacc → 𝑥 ∈ Inaccw ) |
2 |
|
winaon |
⊢ ( 𝑥 ∈ Inaccw → 𝑥 ∈ On ) |
3 |
1 2
|
syl |
⊢ ( 𝑥 ∈ Inacc → 𝑥 ∈ On ) |
4 |
3
|
ssriv |
⊢ Inacc ⊆ On |
5 |
|
ssorduni |
⊢ ( Inacc ⊆ On → Ord ∪ Inacc ) |
6 |
|
ordsson |
⊢ ( Ord ∪ Inacc → ∪ Inacc ⊆ On ) |
7 |
4 5 6
|
mp2b |
⊢ ∪ Inacc ⊆ On |
8 |
|
vex |
⊢ 𝑦 ∈ V |
9 |
|
grothtsk |
⊢ ∪ Tarski = V |
10 |
8 9
|
eleqtrri |
⊢ 𝑦 ∈ ∪ Tarski |
11 |
|
eluni2 |
⊢ ( 𝑦 ∈ ∪ Tarski ↔ ∃ 𝑤 ∈ Tarski 𝑦 ∈ 𝑤 ) |
12 |
10 11
|
mpbi |
⊢ ∃ 𝑤 ∈ Tarski 𝑦 ∈ 𝑤 |
13 |
|
ne0i |
⊢ ( 𝑦 ∈ 𝑤 → 𝑤 ≠ ∅ ) |
14 |
|
tskcard |
⊢ ( ( 𝑤 ∈ Tarski ∧ 𝑤 ≠ ∅ ) → ( card ‘ 𝑤 ) ∈ Inacc ) |
15 |
13 14
|
sylan2 |
⊢ ( ( 𝑤 ∈ Tarski ∧ 𝑦 ∈ 𝑤 ) → ( card ‘ 𝑤 ) ∈ Inacc ) |
16 |
|
tsksdom |
⊢ ( ( 𝑤 ∈ Tarski ∧ 𝑦 ∈ 𝑤 ) → 𝑦 ≺ 𝑤 ) |
17 |
16
|
adantl |
⊢ ( ( 𝑦 ∈ On ∧ ( 𝑤 ∈ Tarski ∧ 𝑦 ∈ 𝑤 ) ) → 𝑦 ≺ 𝑤 ) |
18 |
|
tskwe2 |
⊢ ( 𝑤 ∈ Tarski → 𝑤 ∈ dom card ) |
19 |
18
|
adantr |
⊢ ( ( 𝑤 ∈ Tarski ∧ 𝑦 ∈ 𝑤 ) → 𝑤 ∈ dom card ) |
20 |
|
cardsdomel |
⊢ ( ( 𝑦 ∈ On ∧ 𝑤 ∈ dom card ) → ( 𝑦 ≺ 𝑤 ↔ 𝑦 ∈ ( card ‘ 𝑤 ) ) ) |
21 |
19 20
|
sylan2 |
⊢ ( ( 𝑦 ∈ On ∧ ( 𝑤 ∈ Tarski ∧ 𝑦 ∈ 𝑤 ) ) → ( 𝑦 ≺ 𝑤 ↔ 𝑦 ∈ ( card ‘ 𝑤 ) ) ) |
22 |
17 21
|
mpbid |
⊢ ( ( 𝑦 ∈ On ∧ ( 𝑤 ∈ Tarski ∧ 𝑦 ∈ 𝑤 ) ) → 𝑦 ∈ ( card ‘ 𝑤 ) ) |
23 |
|
eleq2 |
⊢ ( 𝑧 = ( card ‘ 𝑤 ) → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ ( card ‘ 𝑤 ) ) ) |
24 |
23
|
rspcev |
⊢ ( ( ( card ‘ 𝑤 ) ∈ Inacc ∧ 𝑦 ∈ ( card ‘ 𝑤 ) ) → ∃ 𝑧 ∈ Inacc 𝑦 ∈ 𝑧 ) |
25 |
15 22 24
|
syl2an2 |
⊢ ( ( 𝑦 ∈ On ∧ ( 𝑤 ∈ Tarski ∧ 𝑦 ∈ 𝑤 ) ) → ∃ 𝑧 ∈ Inacc 𝑦 ∈ 𝑧 ) |
26 |
25
|
rexlimdvaa |
⊢ ( 𝑦 ∈ On → ( ∃ 𝑤 ∈ Tarski 𝑦 ∈ 𝑤 → ∃ 𝑧 ∈ Inacc 𝑦 ∈ 𝑧 ) ) |
27 |
12 26
|
mpi |
⊢ ( 𝑦 ∈ On → ∃ 𝑧 ∈ Inacc 𝑦 ∈ 𝑧 ) |
28 |
|
eluni2 |
⊢ ( 𝑦 ∈ ∪ Inacc ↔ ∃ 𝑧 ∈ Inacc 𝑦 ∈ 𝑧 ) |
29 |
27 28
|
sylibr |
⊢ ( 𝑦 ∈ On → 𝑦 ∈ ∪ Inacc ) |
30 |
29
|
ssriv |
⊢ On ⊆ ∪ Inacc |
31 |
7 30
|
eqssi |
⊢ ∪ Inacc = On |
32 |
|
ssonprc |
⊢ ( Inacc ⊆ On → ( Inacc ∉ V ↔ ∪ Inacc = On ) ) |
33 |
4 32
|
ax-mp |
⊢ ( Inacc ∉ V ↔ ∪ Inacc = On ) |
34 |
31 33
|
mpbir |
⊢ Inacc ∉ V |