Metamath Proof Explorer

Theorem inf3lema

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 inf3lema 
|- ( A e. ( G ` B ) <-> ( A e. x /\ ( A i^i x ) C_ B ) )

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 ineq1 
 |-  ( f = A -> ( f i^i x ) = ( A i^i x ) )
6 5 sseq1d 
 |-  ( f = A -> ( ( f i^i x ) C_ B <-> ( A i^i x ) C_ B ) )
7 sseq2 
 |-  ( v = B -> ( ( f i^i x ) C_ v <-> ( f i^i x ) C_ B ) )
8 7 rabbidv 
 |-  ( v = B -> { f e. x | ( f i^i x ) C_ v } = { f e. x | ( f i^i x ) C_ B } )
9 sseq2 
 |-  ( y = v -> ( ( w i^i x ) C_ y <-> ( w i^i x ) C_ v ) )
10 9 rabbidv 
 |-  ( y = v -> { w e. x | ( w i^i x ) C_ y } = { w e. x | ( w i^i x ) C_ v } )
11 ineq1 
 |-  ( w = f -> ( w i^i x ) = ( f i^i x ) )
12 11 sseq1d 
 |-  ( w = f -> ( ( w i^i x ) C_ v <-> ( f i^i x ) C_ v ) )
13 12 cbvrabv 
 |-  { w e. x | ( w i^i x ) C_ v } = { f e. x | ( f i^i x ) C_ v }
14 10 13 eqtrdi 
 |-  ( y = v -> { w e. x | ( w i^i x ) C_ y } = { f e. x | ( f i^i x ) C_ v } )
15 14 cbvmptv 
 |-  ( y e. _V |-> { w e. x | ( w i^i x ) C_ y } ) = ( v e. _V |-> { f e. x | ( f i^i x ) C_ v } )
16 1 15 eqtri 
 |-  G = ( v e. _V |-> { f e. x | ( f i^i x ) C_ v } )
17 vex 
 |-  x e. _V
18 17 rabex 
 |-  { f e. x | ( f i^i x ) C_ B } e. _V
19 8 16 18 fvmpt 
 |-  ( B e. _V -> ( G ` B ) = { f e. x | ( f i^i x ) C_ B } )
20 4 19 ax-mp 
 |-  ( G ` B ) = { f e. x | ( f i^i x ) C_ B }
21 6 20 elrab2 
 |-  ( A e. ( G ` B ) <-> ( A e. x /\ ( A i^i x ) C_ B ) )