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 e/ _V

Proof

Step Hyp Ref Expression
1 inawina 
 |-  ( x e. Inacc -> x e. InaccW )
2 winaon 
 |-  ( x e. InaccW -> x e. On )
3 1 2 syl 
 |-  ( x e. Inacc -> x e. On )
4 3 ssriv 
 |-  Inacc C_ On
5 ssorduni 
 |-  ( Inacc C_ On -> Ord U. Inacc )
6 ordsson 
 |-  ( Ord U. Inacc -> U. Inacc C_ On )
7 4 5 6 mp2b 
 |-  U. Inacc C_ On
8 vex 
 |-  y e. _V
9 grothtsk 
 |-  U. Tarski = _V
10 8 9 eleqtrri 
 |-  y e. U. Tarski
11 eluni2 
 |-  ( y e. U. Tarski <-> E. w e. Tarski y e. w )
12 10 11 mpbi 
 |-  E. w e. Tarski y e. w
13 ne0i 
 |-  ( y e. w -> w =/= (/) )
14 tskcard 
 |-  ( ( w e. Tarski /\ w =/= (/) ) -> ( card ` w ) e. Inacc )
15 13 14 sylan2 
 |-  ( ( w e. Tarski /\ y e. w ) -> ( card ` w ) e. Inacc )
16 tsksdom 
 |-  ( ( w e. Tarski /\ y e. w ) -> y ~< w )
17 16 adantl 
 |-  ( ( y e. On /\ ( w e. Tarski /\ y e. w ) ) -> y ~< w )
18 tskwe2 
 |-  ( w e. Tarski -> w e. dom card )
19 18 adantr 
 |-  ( ( w e. Tarski /\ y e. w ) -> w e. dom card )
20 cardsdomel 
 |-  ( ( y e. On /\ w e. dom card ) -> ( y ~< w <-> y e. ( card ` w ) ) )
21 19 20 sylan2 
 |-  ( ( y e. On /\ ( w e. Tarski /\ y e. w ) ) -> ( y ~< w <-> y e. ( card ` w ) ) )
22 17 21 mpbid 
 |-  ( ( y e. On /\ ( w e. Tarski /\ y e. w ) ) -> y e. ( card ` w ) )
23 eleq2 
 |-  ( z = ( card ` w ) -> ( y e. z <-> y e. ( card ` w ) ) )
24 23 rspcev 
 |-  ( ( ( card ` w ) e. Inacc /\ y e. ( card ` w ) ) -> E. z e. Inacc y e. z )
25 15 22 24 syl2an2 
 |-  ( ( y e. On /\ ( w e. Tarski /\ y e. w ) ) -> E. z e. Inacc y e. z )
26 25 rexlimdvaa 
 |-  ( y e. On -> ( E. w e. Tarski y e. w -> E. z e. Inacc y e. z ) )
27 12 26 mpi 
 |-  ( y e. On -> E. z e. Inacc y e. z )
28 eluni2 
 |-  ( y e. U. Inacc <-> E. z e. Inacc y e. z )
29 27 28 sylibr 
 |-  ( y e. On -> y e. U. Inacc )
30 29 ssriv 
 |-  On C_ U. Inacc
31 7 30 eqssi 
 |-  U. Inacc = On
32 ssonprc 
 |-  ( Inacc C_ On -> ( Inacc e/ _V <-> U. Inacc = On ) )
33 4 32 ax-mp 
 |-  ( Inacc e/ _V <-> U. Inacc = On )
34 31 33 mpbir 
 |-  Inacc e/ _V