Metamath Proof Explorer

Theorem inf3lemd

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 inf3lemd 
|- ( A e. _om -> ( F ` A ) C_ x )

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 
 |-  ( A = (/) -> ( F ` A ) = ( F ` (/) ) )
6 1 2 3 4 inf3lemb 
 |-  ( F ` (/) ) = (/)
7 5 6 eqtrdi 
 |-  ( A = (/) -> ( F ` A ) = (/) )
8 0ss 
 |-  (/) C_ x
9 7 8 eqsstrdi 
 |-  ( A = (/) -> ( F ` A ) C_ x )
10 9 a1d 
 |-  ( A = (/) -> ( A e. _om -> ( F ` A ) C_ x ) )
11 nnsuc 
 |-  ( ( A e. _om /\ A =/= (/) ) -> E. v e. _om A = suc v )
12 vex 
 |-  v e. _V
13 1 2 12 4 inf3lemc 
 |-  ( v e. _om -> ( F ` suc v ) = ( G ` ( F ` v ) ) )
14 13 eleq2d 
 |-  ( v e. _om -> ( u e. ( F ` suc v ) <-> u e. ( G ` ( F ` v ) ) ) )
15 vex 
 |-  u e. _V
16 fvex 
 |-  ( F ` v ) e. _V
17 1 2 15 16 inf3lema 
 |-  ( u e. ( G ` ( F ` v ) ) <-> ( u e. x /\ ( u i^i x ) C_ ( F ` v ) ) )
18 17 simplbi 
 |-  ( u e. ( G ` ( F ` v ) ) -> u e. x )
19 14 18 biimtrdi 
 |-  ( v e. _om -> ( u e. ( F ` suc v ) -> u e. x ) )
20 19 ssrdv 
 |-  ( v e. _om -> ( F ` suc v ) C_ x )
21 fveq2 
 |-  ( A = suc v -> ( F ` A ) = ( F ` suc v ) )
22 21 sseq1d 
 |-  ( A = suc v -> ( ( F ` A ) C_ x <-> ( F ` suc v ) C_ x ) )
23 20 22 syl5ibrcom 
 |-  ( v e. _om -> ( A = suc v -> ( F ` A ) C_ x ) )
24 23 rexlimiv 
 |-  ( E. v e. _om A = suc v -> ( F ` A ) C_ x )
25 11 24 syl 
 |-  ( ( A e. _om /\ A =/= (/) ) -> ( F ` A ) C_ x )
26 25 expcom 
 |-  ( A =/= (/) -> ( A e. _om -> ( F ` A ) C_ x ) )
27 10 26 pm2.61ine 
 |-  ( A e. _om -> ( F ` A ) C_ x )