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 biimpri 
 |-  ( (/) e. y -> ( R1 ` (/) ) e. y )
19 18 adantr 
 |-  ( ( (/) e. y /\ A. z e. y ~P z e. y ) -> ( R1 ` (/) ) e. y )
20 pweq 
 |-  ( z = ( R1 ` w ) -> ~P z = ~P ( R1 ` w ) )
21 20 eleq1d 
 |-  ( z = ( R1 ` w ) -> ( ~P z e. y <-> ~P ( R1 ` w ) e. y ) )
22 21 rspccv 
 |-  ( A. z e. y ~P z e. y -> ( ( R1 ` w ) e. y -> ~P ( R1 ` w ) e. y ) )
23 nnon 
 |-  ( w e. _om -> w e. On )
24 r1suc 
 |-  ( w e. On -> ( R1 ` suc w ) = ~P ( R1 ` w ) )
25 23 24 syl 
 |-  ( w e. _om -> ( R1 ` suc w ) = ~P ( R1 ` w ) )
26 25 eleq1d 
 |-  ( w e. _om -> ( ( R1 ` suc w ) e. y <-> ~P ( R1 ` w ) e. y ) )
27 26 biimprcd 
 |-  ( ~P ( R1 ` w ) e. y -> ( w e. _om -> ( R1 ` suc w ) e. y ) )
28 22 27 syl6 
 |-  ( A. z e. y ~P z e. y -> ( ( R1 ` w ) e. y -> ( w e. _om -> ( R1 ` suc w ) e. y ) ) )
29 28 com3r 
 |-  ( w e. _om -> ( A. z e. y ~P z e. y -> ( ( R1 ` w ) e. y -> ( R1 ` suc w ) e. y ) ) )
30 29 adantld 
 |-  ( w e. _om -> ( ( (/) e. y /\ A. z e. y ~P z e. y ) -> ( ( R1 ` w ) e. y -> ( R1 ` suc w ) e. y ) ) )
31 11 13 15 19 30 finds2 
 |-  ( x e. _om -> ( ( (/) e. y /\ A. z e. y ~P z e. y ) -> ( R1 ` x ) e. y ) )
32 eleq1 
 |-  ( ( R1 ` x ) = w -> ( ( R1 ` x ) e. y <-> w e. y ) )
33 32 biimpd 
 |-  ( ( R1 ` x ) = w -> ( ( R1 ` x ) e. y -> w e. y ) )
34 31 33 syl9 
 |-  ( x e. _om -> ( ( R1 ` x ) = w -> ( ( (/) e. y /\ A. z e. y ~P z e. y ) -> w e. y ) ) )
35 34 rexlimiv 
 |-  ( E. x e. _om ( R1 ` x ) = w -> ( ( (/) e. y /\ A. z e. y ~P z e. y ) -> w e. y ) )
36 9 35 sylbi 
 |-  ( w e. ( R1 " _om ) -> ( ( (/) e. y /\ A. z e. y ~P z e. y ) -> w e. y ) )
37 36 com12 
 |-  ( ( (/) e. y /\ A. z e. y ~P z e. y ) -> ( w e. ( R1 " _om ) -> w e. y ) )
38 37 ssrdv 
 |-  ( ( (/) e. y /\ A. z e. y ~P z e. y ) -> ( R1 " _om ) C_ y )
39 vex 
 |-  y e. _V
40 39 ssex 
 |-  ( ( R1 " _om ) C_ y -> ( R1 " _om ) e. _V )
41 38 40 syl 
 |-  ( ( (/) e. y /\ A. z e. y ~P z e. y ) -> ( R1 " _om ) e. _V )
42 0ex 
 |-  (/) e. _V
43 eleq1 
 |-  ( x = (/) -> ( x e. y <-> (/) e. y ) )
44 43 anbi1d 
 |-  ( x = (/) -> ( ( x e. y /\ A. z e. y ~P z e. y ) <-> ( (/) e. y /\ A. z e. y ~P z e. y ) ) )
45 44 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 ) ) )
46 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 ) )
47 simpr 
 |-  ( ( ~P z C_ y /\ ~P z e. y ) -> ~P z e. y )
48 47 ralimi 
 |-  ( A. z e. y ( ~P z C_ y /\ ~P z e. y ) -> A. z e. y ~P z e. y )
49 48 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 ) )
50 49 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 ) )
51 46 50 eximii 
 |-  E. y ( x e. y /\ A. z e. y ~P z e. y )
52 42 45 51 vtocl 
 |-  E. y ( (/) e. y /\ A. z e. y ~P z e. y )
53 41 52 exlimiiv 
 |-  ( R1 " _om ) e. _V
54 f1dmex 
 |-  ( ( ( R1 |` _om ) : _om -1-1-> ( R1 " _om ) /\ ( R1 " _om ) e. _V ) -> _om e. _V )
55 6 53 54 mp2an 
 |-  _om e. _V