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

Metamath Proof Explorer

Theorem rdgeq1

Description: Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995) (Revised by Mario Carneiro, 9-May-2015)

Ref Expression
Assertion rdgeq1 ( 𝐹 = 𝐺 → rec ( 𝐹 , 𝐴 ) = rec ( 𝐺 , 𝐴 ) )

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ ( 𝐹 = 𝐺 → ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) = ( 𝐺 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) )
2 1 ifeq2d ⊢ ( 𝐹 = 𝐺 → if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) = if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐺 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) )
3 2 ifeq2d ⊢ ( 𝐹 = 𝐺 → if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) = if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐺 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) )
4 3 mpteq2dv ⊢ ( 𝐹 = 𝐺 → ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) = ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐺 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) )
5 recseq ⊢ ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) = ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐺 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) → recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ) = recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐺 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ) )
6 4 5 syl ⊢ ( 𝐹 = 𝐺 → recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ) = recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐺 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) ) )
7 df-rdg ⊢ rec ( 𝐹 , 𝐴 ) = recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐹 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) )
8 df-rdg ⊢ rec ( 𝐺 , 𝐴 ) = recs ( ( 𝑔 ∈ V ↦ if ( 𝑔 = ∅ , 𝐴 , if ( Lim dom 𝑔 , ∪ ran 𝑔 , ( 𝐺 ‘ ( 𝑔 ‘ ∪ dom 𝑔 ) ) ) ) ) )
9 6 7 8 3eqtr4g ⊢ ( 𝐹 = 𝐺 → rec ( 𝐹 , 𝐴 ) = rec ( 𝐺 , 𝐴 ) )