Theorem inf3lem4

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. (Contributed by NM, 29-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	inf3lem4	|- ( ( x =/= (/) /\ x C_ U. x ) -> ( 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	1 2 3 4	inf3lem1	|- ( A e. _om -> ( F ` A ) C_ ( F ` suc A ) )
6	5	a1i	|- ( ( x =/= (/) /\ x C_ U. x ) -> ( A e. _om -> ( F ` A ) C_ ( F ` suc A ) ) )
7	1 2 3 4	inf3lem3	|- ( ( x =/= (/) /\ x C_ U. x ) -> ( A e. _om -> ( F ` A ) =/= ( F ` suc A ) ) )
8	6 7	jcad	|- ( ( x =/= (/) /\ x C_ U. x ) -> ( A e. _om -> ( ( F ` A ) C_ ( F ` suc A ) /\ ( F ` A ) =/= ( F ` suc A ) ) ) )
9		df-pss	|- ( ( F ` A ) C. ( F ` suc A ) <-> ( ( F ` A ) C_ ( F ` suc A ) /\ ( F ` A ) =/= ( F ` suc A ) ) )
10	8 9	syl6ibr	|- ( ( x =/= (/) /\ x C_ U. x ) -> ( A e. _om -> ( F ` A ) C. ( F ` suc A ) ) )