Metamath Proof Explorer

Theorem inaprc

Description: An equivalent to the Tarski-Grothendieck Axiom: there is a proper class of inaccessible cardinals. (Contributed by Mario Carneiro, 9-Jun-2013)

Ref Expression
Assertion inaprc ⊢ Inacc ∉ V

Proof

Step Hyp Ref Expression
1 inawina ⊢ x ∈ Inacc → x ∈ Inacc 𝑤
2 winaon ⊢ x ∈ Inacc 𝑤 → x ∈ On
3 1 2 syl ⊢ x ∈ Inacc → x ∈ 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 ⊢ y ∈ V
9 grothtsk ⊢ ⋃ Tarski = V
10 8 9 eleqtrri ⊢ y ∈ ⋃ Tarski
11 eluni2 ⊢ y ∈ ⋃ Tarski ↔ ∃ w ∈ Tarski y ∈ w
12 10 11 mpbi ⊢ ∃ w ∈ Tarski y ∈ w
13 ne0i ⊢ y ∈ w → w ≠ ∅
14 tskcard ⊢ w ∈ Tarski ∧ w ≠ ∅ → card ⁡ w ∈ Inacc
15 13 14 sylan2 ⊢ w ∈ Tarski ∧ y ∈ w → card ⁡ w ∈ Inacc
16 tsksdom ⊢ w ∈ Tarski ∧ y ∈ w → y ≺ w
17 16 adantl ⊢ y ∈ On ∧ w ∈ Tarski ∧ y ∈ w → y ≺ w
18 tskwe2 ⊢ w ∈ Tarski → w ∈ dom ⁡ card
19 18 adantr ⊢ w ∈ Tarski ∧ y ∈ w → w ∈ dom ⁡ card
20 cardsdomel ⊢ y ∈ On ∧ w ∈ dom ⁡ card → y ≺ w ↔ y ∈ card ⁡ w
21 19 20 sylan2 ⊢ y ∈ On ∧ w ∈ Tarski ∧ y ∈ w → y ≺ w ↔ y ∈ card ⁡ w
22 17 21 mpbid ⊢ y ∈ On ∧ w ∈ Tarski ∧ y ∈ w → y ∈ card ⁡ w
23 eleq2 ⊢ z = card ⁡ w → y ∈ z ↔ y ∈ card ⁡ w
24 23 rspcev ⊢ card ⁡ w ∈ Inacc ∧ y ∈ card ⁡ w → ∃ z ∈ Inacc y ∈ z
25 15 22 24 syl2an2 ⊢ y ∈ On ∧ w ∈ Tarski ∧ y ∈ w → ∃ z ∈ Inacc y ∈ z
26 25 rexlimdvaa ⊢ y ∈ On → ∃ w ∈ Tarski y ∈ w → ∃ z ∈ Inacc y ∈ z
27 12 26 mpi ⊢ y ∈ On → ∃ z ∈ Inacc y ∈ z
28 eluni2 ⊢ y ∈ ⋃ Inacc ↔ ∃ z ∈ Inacc y ∈ z
29 27 28 sylibr ⊢ y ∈ On → y ∈ ⋃ 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