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 ( 𝑥 ∈ 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