This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem inf3lemc

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 inf3lemc 
|- ( A e. _om -> ( F ` suc A ) = ( G ` ( F ` 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 frsuc 
 |-  ( A e. _om -> ( ( rec ( G , (/) ) |` _om ) ` suc A ) = ( G ` ( ( rec ( G , (/) ) |` _om ) ` A ) ) )
6 2 fveq1i 
 |-  ( F ` suc A ) = ( ( rec ( G , (/) ) |` _om ) ` suc A )
7 2 fveq1i 
 |-  ( F ` A ) = ( ( rec ( G , (/) ) |` _om ) ` A )
8 7 fveq2i 
 |-  ( G ` ( F ` A ) ) = ( G ` ( ( rec ( G , (/) ) |` _om ) ` A ) )
9 5 6 8 3eqtr4g 
 |-  ( A e. _om -> ( F ` suc A ) = ( G ` ( F ` A ) ) )