This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐴 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝐴 ) ) )