Theorem inf3lemb

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	inf3lemb	|- ( F ` (/) ) = (/)

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	2	fveq1i	|- ( F ` (/) ) = ( ( rec ( G , (/) ) |` _om ) ` (/) )
6		0ex	|- (/) e. _V
7		fr0g	|- ( (/) e. _V -> ( ( rec ( G , (/) ) |` _om ) ` (/) ) = (/) )
8	6 7	ax-mp	|- ( ( rec ( G , (/) ) |` _om ) ` (/) ) = (/)
9	5 8	eqtri	|- ( F ` (/) ) = (/)