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∈Tarskiy∈w
12 10 11 mpbi ⊢∃w∈Tarskiy∈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∈Inaccy∈z
25 15 22 24 syl2an2 ⊢y∈On∧w∈Tarski∧y∈w→∃z∈Inaccy∈z
26 25 rexlimdvaa ⊢y∈On→∃w∈Tarskiy∈w→∃z∈Inaccy∈z
27 12 26 mpi ⊢y∈On→∃z∈Inaccy∈z
28 eluni2 ⊢y∈⋃Inacc↔∃z∈Inaccy∈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