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

Proof

Step	Hyp	Ref	Expression
1		inf3lem.1	⊢ 𝐺 = ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } )
2		inf3lem.2	⊢ 𝐹 = ( rec ( 𝐺 , ∅ ) ↾ ω )
3		inf3lem.3	⊢ 𝐴 ∈ V
4		inf3lem.4	⊢ 𝐵 ∈ V
5		frsuc	⊢ ( 𝐴 ∈ ω → ( ( rec ( 𝐺 , ∅ ) ↾ ω ) ‘ suc 𝐴 ) = ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ↾ ω ) ‘ 𝐴 ) ) )
6	2	fveq1i	⊢ ( 𝐹 ‘ suc 𝐴 ) = ( ( rec ( 𝐺 , ∅ ) ↾ ω ) ‘ suc 𝐴 )
7	2	fveq1i	⊢ ( 𝐹 ‘ 𝐴 ) = ( ( rec ( 𝐺 , ∅ ) ↾ ω ) ‘ 𝐴 )
8	7	fveq2i	⊢ ( 𝐺 ‘ ( 𝐹 ‘ 𝐴 ) ) = ( 𝐺 ‘ ( ( rec ( 𝐺 , ∅ ) ↾ ω ) ‘ 𝐴 ) )
9	5 6 8	3eqtr4g	⊢ ( 𝐴 ∈ ω → ( 𝐹 ‘ suc 𝐴 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝐴 ) ) )