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 ) )