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 ⊢ F = G → rec ⁡ F A = rec ⁡ G A

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ F = G → F ⁡ g ⁡ ⋃ dom ⁡ g = G ⁡ g ⁡ ⋃ dom ⁡ g
2 1 ifeq2d ⊢ F = G → if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g G ⁡ g ⁡ ⋃ dom ⁡ g
3 2 ifeq2d ⊢ F = G → if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g G ⁡ g ⁡ ⋃ dom ⁡ g
4 3 mpteq2dv ⊢ F = G → g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g G ⁡ g ⁡ ⋃ dom ⁡ g
5 recseq ⊢ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g G ⁡ g ⁡ ⋃ dom ⁡ g → recs ⁡ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = recs ⁡ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g G ⁡ g ⁡ ⋃ dom ⁡ g
6 4 5 syl ⊢ F = G → recs ⁡ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = recs ⁡ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g G ⁡ g ⁡ ⋃ dom ⁡ g
7 df-rdg ⊢ rec ⁡ F A = recs ⁡ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
8 df-rdg ⊢ rec ⁡ G A = recs ⁡ g ∈ V ⟼ if g = ∅ A if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g G ⁡ g ⁡ ⋃ dom ⁡ g
9 6 7 8 3eqtr4g ⊢ F = G → rec ⁡ F A = rec ⁡ G A