Metamath Proof Explorer

Theorem inf3lem1

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. (Contributed by NM, 28-Oct-1996)

Ref Expression
Hypotheses inf3lem.1 
|- G = ( y e. _V |-> { w e. x | ( w i^i x ) C_ y } )
inf3lem.2 
|- F = ( rec ( G , (/) ) |` _om )
inf3lem.3 
|- A e. _V
inf3lem.4 
|- B e. _V
Assertion inf3lem1 
|- ( A e. _om -> ( F ` A ) C_ ( F ` suc A ) )

Proof

Step Hyp Ref Expression
1 inf3lem.1 
 |-  G = ( y e. _V |-> { w e. x | ( w i^i x ) C_ y } )
2 inf3lem.2 
 |-  F = ( rec ( G , (/) ) |` _om )
3 inf3lem.3 
 |-  A e. _V
4 inf3lem.4 
 |-  B e. _V
5 fveq2 
 |-  ( v = (/) -> ( F ` v ) = ( F ` (/) ) )
6 suceq 
 |-  ( v = (/) -> suc v = suc (/) )
7 6 fveq2d 
 |-  ( v = (/) -> ( F ` suc v ) = ( F ` suc (/) ) )
8 5 7 sseq12d 
 |-  ( v = (/) -> ( ( F ` v ) C_ ( F ` suc v ) <-> ( F ` (/) ) C_ ( F ` suc (/) ) ) )
9 fveq2 
 |-  ( v = u -> ( F ` v ) = ( F ` u ) )
10 suceq 
 |-  ( v = u -> suc v = suc u )
11 10 fveq2d 
 |-  ( v = u -> ( F ` suc v ) = ( F ` suc u ) )
12 9 11 sseq12d 
 |-  ( v = u -> ( ( F ` v ) C_ ( F ` suc v ) <-> ( F ` u ) C_ ( F ` suc u ) ) )
13 fveq2 
 |-  ( v = suc u -> ( F ` v ) = ( F ` suc u ) )
14 suceq 
 |-  ( v = suc u -> suc v = suc suc u )
15 14 fveq2d 
 |-  ( v = suc u -> ( F ` suc v ) = ( F ` suc suc u ) )
16 13 15 sseq12d 
 |-  ( v = suc u -> ( ( F ` v ) C_ ( F ` suc v ) <-> ( F ` suc u ) C_ ( F ` suc suc u ) ) )
17 fveq2 
 |-  ( v = A -> ( F ` v ) = ( F ` A ) )
18 suceq 
 |-  ( v = A -> suc v = suc A )
19 18 fveq2d 
 |-  ( v = A -> ( F ` suc v ) = ( F ` suc A ) )
20 17 19 sseq12d 
 |-  ( v = A -> ( ( F ` v ) C_ ( F ` suc v ) <-> ( F ` A ) C_ ( F ` suc A ) ) )
21 1 2 3 3 inf3lemb 
 |-  ( F ` (/) ) = (/)
22 0ss 
 |-  (/) C_ ( F ` suc (/) )
23 21 22 eqsstri 
 |-  ( F ` (/) ) C_ ( F ` suc (/) )
24 sstr2 
 |-  ( ( v i^i x ) C_ ( F ` u ) -> ( ( F ` u ) C_ ( F ` suc u ) -> ( v i^i x ) C_ ( F ` suc u ) ) )
25 24 com12 
 |-  ( ( F ` u ) C_ ( F ` suc u ) -> ( ( v i^i x ) C_ ( F ` u ) -> ( v i^i x ) C_ ( F ` suc u ) ) )
26 25 anim2d 
 |-  ( ( F ` u ) C_ ( F ` suc u ) -> ( ( v e. x /\ ( v i^i x ) C_ ( F ` u ) ) -> ( v e. x /\ ( v i^i x ) C_ ( F ` suc u ) ) ) )
27 vex 
 |-  u e. _V
28 1 2 27 3 inf3lemc 
 |-  ( u e. _om -> ( F ` suc u ) = ( G ` ( F ` u ) ) )
29 28 eleq2d 
 |-  ( u e. _om -> ( v e. ( F ` suc u ) <-> v e. ( G ` ( F ` u ) ) ) )
30 vex 
 |-  v e. _V
31 fvex 
 |-  ( F ` u ) e. _V
32 1 2 30 31 inf3lema 
 |-  ( v e. ( G ` ( F ` u ) ) <-> ( v e. x /\ ( v i^i x ) C_ ( F ` u ) ) )
33 29 32 bitrdi 
 |-  ( u e. _om -> ( v e. ( F ` suc u ) <-> ( v e. x /\ ( v i^i x ) C_ ( F ` u ) ) ) )
34 peano2b 
 |-  ( u e. _om <-> suc u e. _om )
35 27 sucex 
 |-  suc u e. _V
36 1 2 35 3 inf3lemc 
 |-  ( suc u e. _om -> ( F ` suc suc u ) = ( G ` ( F ` suc u ) ) )
37 34 36 sylbi 
 |-  ( u e. _om -> ( F ` suc suc u ) = ( G ` ( F ` suc u ) ) )
38 37 eleq2d 
 |-  ( u e. _om -> ( v e. ( F ` suc suc u ) <-> v e. ( G ` ( F ` suc u ) ) ) )
39 fvex 
 |-  ( F ` suc u ) e. _V
40 1 2 30 39 inf3lema 
 |-  ( v e. ( G ` ( F ` suc u ) ) <-> ( v e. x /\ ( v i^i x ) C_ ( F ` suc u ) ) )
41 38 40 bitrdi 
 |-  ( u e. _om -> ( v e. ( F ` suc suc u ) <-> ( v e. x /\ ( v i^i x ) C_ ( F ` suc u ) ) ) )
42 33 41 imbi12d 
 |-  ( u e. _om -> ( ( v e. ( F ` suc u ) -> v e. ( F ` suc suc u ) ) <-> ( ( v e. x /\ ( v i^i x ) C_ ( F ` u ) ) -> ( v e. x /\ ( v i^i x ) C_ ( F ` suc u ) ) ) ) )
43 26 42 syl5ibr 
 |-  ( u e. _om -> ( ( F ` u ) C_ ( F ` suc u ) -> ( v e. ( F ` suc u ) -> v e. ( F ` suc suc u ) ) ) )
44 43 imp 
 |-  ( ( u e. _om /\ ( F ` u ) C_ ( F ` suc u ) ) -> ( v e. ( F ` suc u ) -> v e. ( F ` suc suc u ) ) )
45 44 ssrdv 
 |-  ( ( u e. _om /\ ( F ` u ) C_ ( F ` suc u ) ) -> ( F ` suc u ) C_ ( F ` suc suc u ) )
46 45 ex 
 |-  ( u e. _om -> ( ( F ` u ) C_ ( F ` suc u ) -> ( F ` suc u ) C_ ( F ` suc suc u ) ) )
47 8 12 16 20 23 46 finds 
 |-  ( A e. _om -> ( F ` A ) C_ ( F ` suc A ) )