Metamath Proof Explorer

Theorem grothomex

Description: The Tarski-Grothendieck Axiom implies the Axiom of Infinity (in the form of omex ). Note that our proof depends on neither the Axiom of Infinity nor Regularity. (Contributed by Mario Carneiro, 19-Apr-2013) (New usage is discouraged.)

Ref Expression
Assertion grothomex 
|- _om e. _V

Proof

Step Hyp Ref Expression
1 r111 
 |-  R1 : On -1-1-> _V
2 omsson 
 |-  _om C_ On
3 f1ores 
 |-  ( ( R1 : On -1-1-> _V /\ _om C_ On ) -> ( R1 |` _om ) : _om -1-1-onto-> ( R1 " _om ) )
4 1 2 3 mp2an 
 |-  ( R1 |` _om ) : _om -1-1-onto-> ( R1 " _om )
5 f1of1 
 |-  ( ( R1 |` _om ) : _om -1-1-onto-> ( R1 " _om ) -> ( R1 |` _om ) : _om -1-1-> ( R1 " _om ) )
6 4 5 ax-mp 
 |-  ( R1 |` _om ) : _om -1-1-> ( R1 " _om )
7 r1fnon 
 |-  R1 Fn On
8 fvelimab 
 |-  ( ( R1 Fn On /\ _om C_ On ) -> ( w e. ( R1 " _om ) <-> E. x e. _om ( R1 ` x ) = w ) )
9 7 2 8 mp2an 
 |-  ( w e. ( R1 " _om ) <-> E. x e. _om ( R1 ` x ) = w )
10 fveq2 
 |-  ( x = (/) -> ( R1 ` x ) = ( R1 ` (/) ) )
11 10 eleq1d 
 |-  ( x = (/) -> ( ( R1 ` x ) e. y <-> ( R1 ` (/) ) e. y ) )
12 fveq2 
 |-  ( x = w -> ( R1 ` x ) = ( R1 ` w ) )
13 12 eleq1d 
 |-  ( x = w -> ( ( R1 ` x ) e. y <-> ( R1 ` w ) e. y ) )
14 fveq2 
 |-  ( x = suc w -> ( R1 ` x ) = ( R1 ` suc w ) )
15 14 eleq1d 
 |-  ( x = suc w -> ( ( R1 ` x ) e. y <-> ( R1 ` suc w ) e. y ) )
16 r10 
 |-  ( R1 ` (/) ) = (/)
17 16 eleq1i 
 |-  ( ( R1 ` (/) ) e. y <-> (/) e. y )
18 17 biranri 
 |-  ( ( (/) e. y /\ A. z e. y ~P z e. y ) -> ( R1 ` (/) ) e. y )
19 pweq 
 |-  ( z = ( R1 ` w ) -> ~P z = ~P ( R1 ` w ) )
20 19 eleq1d 
 |-  ( z = ( R1 ` w ) -> ( ~P z e. y <-> ~P ( R1 ` w ) e. y ) )
21 20 rspccv 
 |-  ( A. z e. y ~P z e. y -> ( ( R1 ` w ) e. y -> ~P ( R1 ` w ) e. y ) )
22 nnon 
 |-  ( w e. _om -> w e. On )
23 r1suc 
 |-  ( w e. On -> ( R1 ` suc w ) = ~P ( R1 ` w ) )
24 22 23 syl 
 |-  ( w e. _om -> ( R1 ` suc w ) = ~P ( R1 ` w ) )
25 24 eleq1d 
 |-  ( w e. _om -> ( ( R1 ` suc w ) e. y <-> ~P ( R1 ` w ) e. y ) )
26 25 biimprcd 
 |-  ( ~P ( R1 ` w ) e. y -> ( w e. _om -> ( R1 ` suc w ) e. y ) )
27 21 26 syl6 
 |-  ( A. z e. y ~P z e. y -> ( ( R1 ` w ) e. y -> ( w e. _om -> ( R1 ` suc w ) e. y ) ) )
28 27 com3r 
 |-  ( w e. _om -> ( A. z e. y ~P z e. y -> ( ( R1 ` w ) e. y -> ( R1 ` suc w ) e. y ) ) )
29 28 adantld 
 |-  ( w e. _om -> ( ( (/) e. y /\ A. z e. y ~P z e. y ) -> ( ( R1 ` w ) e. y -> ( R1 ` suc w ) e. y ) ) )
30 11 13 15 18 29 finds2 
 |-  ( x e. _om -> ( ( (/) e. y /\ A. z e. y ~P z e. y ) -> ( R1 ` x ) e. y ) )
31 eleq1 
 |-  ( ( R1 ` x ) = w -> ( ( R1 ` x ) e. y <-> w e. y ) )
32 31 biimpd 
 |-  ( ( R1 ` x ) = w -> ( ( R1 ` x ) e. y -> w e. y ) )
33 30 32 syl9 
 |-  ( x e. _om -> ( ( R1 ` x ) = w -> ( ( (/) e. y /\ A. z e. y ~P z e. y ) -> w e. y ) ) )
34 33 rexlimiv 
 |-  ( E. x e. _om ( R1 ` x ) = w -> ( ( (/) e. y /\ A. z e. y ~P z e. y ) -> w e. y ) )
35 9 34 sylbi 
 |-  ( w e. ( R1 " _om ) -> ( ( (/) e. y /\ A. z e. y ~P z e. y ) -> w e. y ) )
36 35 com12 
 |-  ( ( (/) e. y /\ A. z e. y ~P z e. y ) -> ( w e. ( R1 " _om ) -> w e. y ) )
37 36 ssrdv 
 |-  ( ( (/) e. y /\ A. z e. y ~P z e. y ) -> ( R1 " _om ) C_ y )
38 vex 
 |-  y e. _V
39 38 ssex 
 |-  ( ( R1 " _om ) C_ y -> ( R1 " _om ) e. _V )
40 37 39 syl 
 |-  ( ( (/) e. y /\ A. z e. y ~P z e. y ) -> ( R1 " _om ) e. _V )
41 0ex 
 |-  (/) e. _V
42 eleq1 
 |-  ( x = (/) -> ( x e. y <-> (/) e. y ) )
43 42 anbi1d 
 |-  ( x = (/) -> ( ( x e. y /\ A. z e. y ~P z e. y ) <-> ( (/) e. y /\ A. z e. y ~P z e. y ) ) )
44 43 exbidv 
 |-  ( x = (/) -> ( E. y ( x e. y /\ A. z e. y ~P z e. y ) <-> E. y ( (/) e. y /\ A. z e. y ~P z e. y ) ) )
45 axgroth6 
 |-  E. y ( x e. y /\ A. z e. y ( ~P z C_ y /\ ~P z e. y ) /\ A. z e. ~P y ( z ~< y -> z e. y ) )
46 simpr 
 |-  ( ( ~P z C_ y /\ ~P z e. y ) -> ~P z e. y )
47 46 ralimi 
 |-  ( A. z e. y ( ~P z C_ y /\ ~P z e. y ) -> A. z e. y ~P z e. y )
48 47 anim2i 
 |-  ( ( x e. y /\ A. z e. y ( ~P z C_ y /\ ~P z e. y ) ) -> ( x e. y /\ A. z e. y ~P z e. y ) )
49 48 3adant3 
 |-  ( ( x e. y /\ A. z e. y ( ~P z C_ y /\ ~P z e. y ) /\ A. z e. ~P y ( z ~< y -> z e. y ) ) -> ( x e. y /\ A. z e. y ~P z e. y ) )
50 45 49 eximii 
 |-  E. y ( x e. y /\ A. z e. y ~P z e. y )
51 41 44 50 vtocl 
 |-  E. y ( (/) e. y /\ A. z e. y ~P z e. y )
52 40 51 exlimiiv 
 |-  ( R1 " _om ) e. _V
53 f1dmex 
 |-  ( ( ( R1 |` _om ) : _om -1-1-> ( R1 " _om ) /\ ( R1 " _om ) e. _V ) -> _om e. _V )
54 6 52 53 mp2an 
 |-  _om e. _V