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	⊢ 𝐺 = ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } )
	inf3lem.2	⊢ 𝐹 = ( rec ( 𝐺 , ∅ ) ↾ ω )
	inf3lem.3	⊢ 𝐴 ∈ V
	inf3lem.4	⊢ 𝐵 ∈ V
Assertion	inf3lemb	⊢ ( 𝐹 ‘ ∅ ) = ∅

Proof

Step	Hyp	Ref	Expression
1		inf3lem.1	⊢ 𝐺 = ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } )
2		inf3lem.2	⊢ 𝐹 = ( rec ( 𝐺 , ∅ ) ↾ ω )
3		inf3lem.3	⊢ 𝐴 ∈ V
4		inf3lem.4	⊢ 𝐵 ∈ V
5	2	fveq1i	⊢ ( 𝐹 ‘ ∅ ) = ( ( rec ( 𝐺 , ∅ ) ↾ ω ) ‘ ∅ )
6		0ex	⊢ ∅ ∈ V
7		fr0g	⊢ ( ∅ ∈ V → ( ( rec ( 𝐺 , ∅ ) ↾ ω ) ‘ ∅ ) = ∅ )
8	6 7	ax-mp	⊢ ( ( rec ( 𝐺 , ∅ ) ↾ ω ) ‘ ∅ ) = ∅
9	5 8	eqtri	⊢ ( 𝐹 ‘ ∅ ) = ∅