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 ( 𝐺 , 𝐴 ) )