MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  grothomex Structured version   Visualization version   Unicode version

Theorem grothomex 9251
Description: The Tarski-Grothendieck Axiom implies the Axiom of Infinity (in the form of omex 8145). Note that our proof depends on neither the Axiom of Infinity nor Regularity. (Contributed by Mario Carneiro, 19-Apr-2013.) (New usage is discouraged.)
Assertion
Ref Expression
grothomex  |-  om  e.  _V

Proof of Theorem grothomex
Dummy variables  x  y  z  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 r111 8243 . . . 4  |-  R1 : On
-1-1-> _V
2 omsson 6693 . . . 4  |-  om  C_  On
3 f1ores 5826 . . . 4  |-  ( ( R1 : On -1-1-> _V  /\ 
om  C_  On )  -> 
( R1  |`  om ) : om -1-1-onto-> ( R1 " om ) )
41, 2, 3mp2an 677 . . 3  |-  ( R1  |`  om ) : om -1-1-onto-> ( R1 " om )
5 f1of1 5811 . . 3  |-  ( ( R1  |`  om ) : om -1-1-onto-> ( R1 " om )  ->  ( R1  |`  om ) : om -1-1-> ( R1 " om ) )
64, 5ax-mp 5 . 2  |-  ( R1  |`  om ) : om -1-1-> ( R1 " om )
7 r1fnon 8235 . . . . . . . 8  |-  R1  Fn  On
8 fvelimab 5919 . . . . . . . 8  |-  ( ( R1  Fn  On  /\  om  C_  On )  ->  (
w  e.  ( R1
" om )  <->  E. x  e.  om  ( R1 `  x )  =  w ) )
97, 2, 8mp2an 677 . . . . . . 7  |-  ( w  e.  ( R1 " om )  <->  E. x  e.  om  ( R1 `  x )  =  w )
10 fveq2 5863 . . . . . . . . . . 11  |-  ( x  =  (/)  ->  ( R1
`  x )  =  ( R1 `  (/) ) )
1110eleq1d 2512 . . . . . . . . . 10  |-  ( x  =  (/)  ->  ( ( R1 `  x )  e.  y  <->  ( R1 `  (/) )  e.  y
) )
12 fveq2 5863 . . . . . . . . . . 11  |-  ( x  =  w  ->  ( R1 `  x )  =  ( R1 `  w
) )
1312eleq1d 2512 . . . . . . . . . 10  |-  ( x  =  w  ->  (
( R1 `  x
)  e.  y  <->  ( R1 `  w )  e.  y ) )
14 fveq2 5863 . . . . . . . . . . 11  |-  ( x  =  suc  w  -> 
( R1 `  x
)  =  ( R1
`  suc  w )
)
1514eleq1d 2512 . . . . . . . . . 10  |-  ( x  =  suc  w  -> 
( ( R1 `  x )  e.  y  <-> 
( R1 `  suc  w )  e.  y ) )
16 r10 8236 . . . . . . . . . . . . 13  |-  ( R1
`  (/) )  =  (/)
1716eleq1i 2519 . . . . . . . . . . . 12  |-  ( ( R1 `  (/) )  e.  y  <->  (/)  e.  y )
1817biimpri 210 . . . . . . . . . . 11  |-  ( (/)  e.  y  ->  ( R1
`  (/) )  e.  y )
1918adantr 467 . . . . . . . . . 10  |-  ( (
(/)  e.  y  /\  A. z  e.  y  ~P z  e.  y )  ->  ( R1 `  (/) )  e.  y )
20 pweq 3953 . . . . . . . . . . . . . . 15  |-  ( z  =  ( R1 `  w )  ->  ~P z  =  ~P ( R1 `  w ) )
2120eleq1d 2512 . . . . . . . . . . . . . 14  |-  ( z  =  ( R1 `  w )  ->  ( ~P z  e.  y  <->  ~P ( R1 `  w
)  e.  y ) )
2221rspccv 3146 . . . . . . . . . . . . 13  |-  ( A. z  e.  y  ~P z  e.  y  ->  ( ( R1 `  w
)  e.  y  ->  ~P ( R1 `  w
)  e.  y ) )
23 nnon 6695 . . . . . . . . . . . . . . . 16  |-  ( w  e.  om  ->  w  e.  On )
24 r1suc 8238 . . . . . . . . . . . . . . . 16  |-  ( w  e.  On  ->  ( R1 `  suc  w )  =  ~P ( R1
`  w ) )
2523, 24syl 17 . . . . . . . . . . . . . . 15  |-  ( w  e.  om  ->  ( R1 `  suc  w )  =  ~P ( R1
`  w ) )
2625eleq1d 2512 . . . . . . . . . . . . . 14  |-  ( w  e.  om  ->  (
( R1 `  suc  w )  e.  y  <->  ~P ( R1 `  w
)  e.  y ) )
2726biimprcd 229 . . . . . . . . . . . . 13  |-  ( ~P ( R1 `  w
)  e.  y  -> 
( w  e.  om  ->  ( R1 `  suc  w )  e.  y ) )
2822, 27syl6 34 . . . . . . . . . . . 12  |-  ( A. z  e.  y  ~P z  e.  y  ->  ( ( R1 `  w
)  e.  y  -> 
( w  e.  om  ->  ( R1 `  suc  w )  e.  y ) ) )
2928com3r 82 . . . . . . . . . . 11  |-  ( w  e.  om  ->  ( A. z  e.  y  ~P z  e.  y  ->  ( ( R1 `  w )  e.  y  ->  ( R1 `  suc  w )  e.  y ) ) )
3029adantld 469 . . . . . . . . . 10  |-  ( w  e.  om  ->  (
( (/)  e.  y  /\  A. z  e.  y  ~P z  e.  y )  ->  ( ( R1
`  w )  e.  y  ->  ( R1 ` 
suc  w )  e.  y ) ) )
3111, 13, 15, 19, 30finds2 6718 . . . . . . . . 9  |-  ( x  e.  om  ->  (
( (/)  e.  y  /\  A. z  e.  y  ~P z  e.  y )  ->  ( R1 `  x )  e.  y ) )
32 eleq1 2516 . . . . . . . . . 10  |-  ( ( R1 `  x )  =  w  ->  (
( R1 `  x
)  e.  y  <->  w  e.  y ) )
3332biimpd 211 . . . . . . . . 9  |-  ( ( R1 `  x )  =  w  ->  (
( R1 `  x
)  e.  y  ->  w  e.  y )
)
3431, 33syl9 73 . . . . . . . 8  |-  ( x  e.  om  ->  (
( R1 `  x
)  =  w  -> 
( ( (/)  e.  y  /\  A. z  e.  y  ~P z  e.  y )  ->  w  e.  y ) ) )
3534rexlimiv 2872 . . . . . . 7  |-  ( E. x  e.  om  ( R1 `  x )  =  w  ->  ( ( (/) 
e.  y  /\  A. z  e.  y  ~P z  e.  y )  ->  w  e.  y ) )
369, 35sylbi 199 . . . . . 6  |-  ( w  e.  ( R1 " om )  ->  ( (
(/)  e.  y  /\  A. z  e.  y  ~P z  e.  y )  ->  w  e.  y ) )
3736com12 32 . . . . 5  |-  ( (
(/)  e.  y  /\  A. z  e.  y  ~P z  e.  y )  ->  ( w  e.  ( R1 " om )  ->  w  e.  y ) )
3837ssrdv 3437 . . . 4  |-  ( (
(/)  e.  y  /\  A. z  e.  y  ~P z  e.  y )  ->  ( R1 " om )  C_  y )
39 vex 3047 . . . . 5  |-  y  e. 
_V
4039ssex 4546 . . . 4  |-  ( ( R1 " om )  C_  y  ->  ( R1 " om )  e.  _V )
4138, 40syl 17 . . 3  |-  ( (
(/)  e.  y  /\  A. z  e.  y  ~P z  e.  y )  ->  ( R1 " om )  e.  _V )
42 0ex 4534 . . . 4  |-  (/)  e.  _V
43 eleq1 2516 . . . . . 6  |-  ( x  =  (/)  ->  ( x  e.  y  <->  (/)  e.  y ) )
4443anbi1d 710 . . . . 5  |-  ( x  =  (/)  ->  ( ( x  e.  y  /\  A. z  e.  y  ~P z  e.  y )  <-> 
( (/)  e.  y  /\  A. z  e.  y  ~P z  e.  y ) ) )
4544exbidv 1767 . . . 4  |-  ( 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 9250 . . . . 5  |-  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 463 . . . . . . . 8  |-  ( ( ~P z  C_  y  /\  ~P z  e.  y )  ->  ~P z  e.  y )
4847ralimi 2780 . . . . . . 7  |-  ( A. z  e.  y  ( ~P z  C_  y  /\  ~P z  e.  y
)  ->  A. z  e.  y  ~P z  e.  y )
4948anim2i 572 . . . . . 6  |-  ( ( 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 ) )
50493adant3 1027 . . . . 5  |-  ( ( 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 ) )
5146, 50eximii 1708 . . . 4  |-  E. y
( x  e.  y  /\  A. z  e.  y  ~P z  e.  y )
5242, 45, 51vtocl 3099 . . 3  |-  E. y
( (/)  e.  y  /\  A. z  e.  y  ~P z  e.  y )
5341, 52exlimiiv 1776 . 2  |-  ( R1
" om )  e. 
_V
54 f1dmex 6760 . 2  |-  ( ( ( R1  |`  om ) : om -1-1-> ( R1 " om )  /\  ( R1 " om )  e. 
_V )  ->  om  e.  _V )
556, 53, 54mp2an 677 1  |-  om  e.  _V
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    /\ w3a 984    = wceq 1443   E.wex 1662    e. wcel 1886   A.wral 2736   E.wrex 2737   _Vcvv 3044    C_ wss 3403   (/)c0 3730   ~Pcpw 3950   class class class wbr 4401    |` cres 4835   "cima 4836   Oncon0 5422   suc csuc 5424    Fn wfn 5576   -1-1->wf1 5578   -1-1-onto->wf1o 5580   ` cfv 5581   omcom 6689    ~< csdm 7565   R1cr1 8230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-groth 9245
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-om 6690  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-er 7360  df-en 7567  df-dom 7568  df-sdom 7569  df-r1 8232
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator