Metamath Proof Explorer

Theorem inf0

Description: Existence of _om implies our axiom of infinity ax-inf . The proof shows that the especially contrived class " ` ran ( rec ( ( v e.V |-> suc v ) , x ) |`om ) " exists, is a subset of its union, and contains a given set x (and thus is nonempty). Thus, it provides an example demonstrating that a set y exists with the necessary properties demanded by ax-inf . (Contributed by NM, 15-Oct-1996) Revised to closed form. (Revised by BJ, 20-May-2024)

Ref Expression
Assertion inf0 
|- ( _om e. V -> E. y ( x e. y /\ A. z ( z e. y -> E. w ( z e. w /\ w e. y ) ) ) )

Proof

Step Hyp Ref Expression
1 fr0g 
 |-  ( x e. _V -> ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` (/) ) = x )
2 1 elv 
 |-  ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` (/) ) = x
3 frfnom 
 |-  ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) Fn _om
4 peano1 
 |-  (/) e. _om
5 fnfvelrn 
 |-  ( ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) Fn _om /\ (/) e. _om ) -> ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` (/) ) e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) )
6 3 4 5 mp2an 
 |-  ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` (/) ) e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om )
7 2 6 eqeltrri 
 |-  x e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om )
8 fvelrnb 
 |-  ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) Fn _om -> ( z e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) <-> E. f e. _om ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` f ) = z ) )
9 3 8 ax-mp 
 |-  ( z e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) <-> E. f e. _om ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` f ) = z )
10 fvex 
 |-  ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` f ) e. _V
11 10 sucid 
 |-  ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` f ) e. suc ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` f )
12 10 sucex 
 |-  suc ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` f ) e. _V
13 eqid 
 |-  ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) = ( rec ( ( v e. _V |-> suc v ) , x ) |` _om )
14 suceq 
 |-  ( z = v -> suc z = suc v )
15 suceq 
 |-  ( z = ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` f ) -> suc z = suc ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` f ) )
16 13 14 15 frsucmpt2 
 |-  ( ( f e. _om /\ suc ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` f ) e. _V ) -> ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` suc f ) = suc ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` f ) )
17 12 16 mpan2 
 |-  ( f e. _om -> ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` suc f ) = suc ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` f ) )
18 11 17 eleqtrrid 
 |-  ( f e. _om -> ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` f ) e. ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` suc f ) )
19 eleq1 
 |-  ( ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` f ) = z -> ( ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` f ) e. ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` suc f ) <-> z e. ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` suc f ) ) )
20 18 19 syl5ib 
 |-  ( ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` f ) = z -> ( f e. _om -> z e. ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` suc f ) ) )
21 peano2b 
 |-  ( f e. _om <-> suc f e. _om )
22 fnfvelrn 
 |-  ( ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) Fn _om /\ suc f e. _om ) -> ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` suc f ) e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) )
23 3 22 mpan 
 |-  ( suc f e. _om -> ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` suc f ) e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) )
24 21 23 sylbi 
 |-  ( f e. _om -> ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` suc f ) e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) )
25 20 24 jca2 
 |-  ( ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` f ) = z -> ( f e. _om -> ( z e. ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` suc f ) /\ ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` suc f ) e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ) ) )
26 fvex 
 |-  ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` suc f ) e. _V
27 eleq2 
 |-  ( w = ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` suc f ) -> ( z e. w <-> z e. ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` suc f ) ) )
28 eleq1 
 |-  ( w = ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` suc f ) -> ( w e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) <-> ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` suc f ) e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ) )
29 27 28 anbi12d 
 |-  ( w = ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` suc f ) -> ( ( z e. w /\ w e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ) <-> ( z e. ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` suc f ) /\ ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` suc f ) e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ) ) )
30 26 29 spcev 
 |-  ( ( z e. ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` suc f ) /\ ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` suc f ) e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ) -> E. w ( z e. w /\ w e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ) )
31 25 30 syl6com 
 |-  ( f e. _om -> ( ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` f ) = z -> E. w ( z e. w /\ w e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ) ) )
32 31 rexlimiv 
 |-  ( E. f e. _om ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ` f ) = z -> E. w ( z e. w /\ w e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ) )
33 9 32 sylbi 
 |-  ( z e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) -> E. w ( z e. w /\ w e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ) )
34 33 ax-gen 
 |-  A. z ( z e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) -> E. w ( z e. w /\ w e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ) )
35 fndm 
 |-  ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) Fn _om -> dom ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) = _om )
36 3 35 ax-mp 
 |-  dom ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) = _om
37 id 
 |-  ( _om e. V -> _om e. V )
38 36 37 eqeltrid 
 |-  ( _om e. V -> dom ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) e. V )
39 fnfun 
 |-  ( ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) Fn _om -> Fun ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) )
40 3 39 ax-mp 
 |-  Fun ( rec ( ( v e. _V |-> suc v ) , x ) |` _om )
41 funrnex 
 |-  ( dom ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) e. V -> ( Fun ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) -> ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) e. _V ) )
42 38 40 41 mpisyl 
 |-  ( _om e. V -> ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) e. _V )
43 eleq2 
 |-  ( y = ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) -> ( x e. y <-> x e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ) )
44 eleq2 
 |-  ( y = ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) -> ( z e. y <-> z e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ) )
45 eleq2 
 |-  ( y = ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) -> ( w e. y <-> w e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ) )
46 45 anbi2d 
 |-  ( y = ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) -> ( ( z e. w /\ w e. y ) <-> ( z e. w /\ w e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ) ) )
47 46 exbidv 
 |-  ( y = ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) -> ( E. w ( z e. w /\ w e. y ) <-> E. w ( z e. w /\ w e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ) ) )
48 44 47 imbi12d 
 |-  ( y = ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) -> ( ( z e. y -> E. w ( z e. w /\ w e. y ) ) <-> ( z e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) -> E. w ( z e. w /\ w e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ) ) ) )
49 48 albidv 
 |-  ( y = ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) -> ( A. z ( z e. y -> E. w ( z e. w /\ w e. y ) ) <-> A. z ( z e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) -> E. w ( z e. w /\ w e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ) ) ) )
50 43 49 anbi12d 
 |-  ( y = ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) -> ( ( x e. y /\ A. z ( z e. y -> E. w ( z e. w /\ w e. y ) ) ) <-> ( x e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) /\ A. z ( z e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) -> E. w ( z e. w /\ w e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ) ) ) ) )
51 50 spcegv 
 |-  ( ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) e. _V -> ( ( x e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) /\ A. z ( z e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) -> E. w ( z e. w /\ w e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ) ) ) -> E. y ( x e. y /\ A. z ( z e. y -> E. w ( z e. w /\ w e. y ) ) ) ) )
52 42 51 syl 
 |-  ( _om e. V -> ( ( x e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) /\ A. z ( z e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) -> E. w ( z e. w /\ w e. ran ( rec ( ( v e. _V |-> suc v ) , x ) |` _om ) ) ) ) -> E. y ( x e. y /\ A. z ( z e. y -> E. w ( z e. w /\ w e. y ) ) ) ) )
53 7 34 52 mp2ani 
 |-  ( _om e. V -> E. y ( x e. y /\ A. z ( z e. y -> E. w ( z e. w /\ w e. y ) ) ) )