Metamath Proof Explorer

Theorem csbrdgg

Description: Move class substitution in and out of the recursive function generator. (Contributed by ML, 25-Oct-2020)

Ref Expression
Assertion csbrdgg ⊢ A ∈ V → ⦋ A / x⦌ rec ⁡ F I = rec ⁡ ⦋ A / x⦌ F ⦋ A / x⦌ I

Proof

Step Hyp Ref Expression
1 csbrecsg ⊢ A ∈ V → ⦋ A / x⦌ recs ⁡ g ∈ V ⟼ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = recs ⁡ ⦋ A / x⦌ g ∈ V ⟼ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
2 csbmpt2 ⊢ A ∈ V → ⦋ A / x⦌ g ∈ V ⟼ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = g ∈ V ⟼ ⦋ A / x⦌ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
3 csbif ⊢ ⦋ A / x⦌ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = if [˙A / x]˙ g = ∅ ⦋ A / x⦌ I ⦋ A / x⦌ if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
4 sbcg ⊢ A ∈ V → [˙A / x]˙ g = ∅ ↔ g = ∅
5 csbif ⊢ ⦋ A / x⦌ if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = if [˙A / x]˙ Lim ⁡ dom ⁡ g ⦋ A / x⦌ ⋃ ran ⁡ g ⦋ A / x⦌ F ⁡ g ⁡ ⋃ dom ⁡ g
6 sbcg ⊢ A ∈ V → [˙A / x]˙ Lim ⁡ dom ⁡ g ↔ Lim ⁡ dom ⁡ g
7 csbconstg ⊢ A ∈ V → ⦋ A / x⦌ ⋃ ran ⁡ g = ⋃ ran ⁡ g
8 csbfv12 ⊢ ⦋ A / x⦌ F ⁡ g ⁡ ⋃ dom ⁡ g = ⦋ A / x⦌ F ⁡ ⦋ A / x⦌ g ⁡ ⋃ dom ⁡ g
9 csbconstg ⊢ A ∈ V → ⦋ A / x⦌ g ⁡ ⋃ dom ⁡ g = g ⁡ ⋃ dom ⁡ g
10 9 fveq2d ⊢ A ∈ V → ⦋ A / x⦌ F ⁡ ⦋ A / x⦌ g ⁡ ⋃ dom ⁡ g = ⦋ A / x⦌ F ⁡ g ⁡ ⋃ dom ⁡ g
11 8 10 eqtrid ⊢ A ∈ V → ⦋ A / x⦌ F ⁡ g ⁡ ⋃ dom ⁡ g = ⦋ A / x⦌ F ⁡ g ⁡ ⋃ dom ⁡ g
12 6 7 11 ifbieq12d ⊢ A ∈ V → if [˙A / x]˙ Lim ⁡ dom ⁡ g ⦋ A / x⦌ ⋃ ran ⁡ g ⦋ A / x⦌ F ⁡ g ⁡ ⋃ dom ⁡ g = if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g ⦋ A / x⦌ F ⁡ g ⁡ ⋃ dom ⁡ g
13 5 12 eqtrid ⊢ A ∈ V → ⦋ A / x⦌ if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g ⦋ A / x⦌ F ⁡ g ⁡ ⋃ dom ⁡ g
14 4 13 ifbieq2d ⊢ A ∈ V → if [˙A / x]˙ g = ∅ ⦋ A / x⦌ I ⦋ A / x⦌ if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = if g = ∅ ⦋ A / x⦌ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g ⦋ A / x⦌ F ⁡ g ⁡ ⋃ dom ⁡ g
15 3 14 eqtrid ⊢ A ∈ V → ⦋ A / x⦌ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = if g = ∅ ⦋ A / x⦌ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g ⦋ A / x⦌ F ⁡ g ⁡ ⋃ dom ⁡ g
16 15 mpteq2dv ⊢ A ∈ V → g ∈ V ⟼ ⦋ A / x⦌ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = g ∈ V ⟼ if g = ∅ ⦋ A / x⦌ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g ⦋ A / x⦌ F ⁡ g ⁡ ⋃ dom ⁡ g
17 2 16 eqtrd ⊢ A ∈ V → ⦋ A / x⦌ g ∈ V ⟼ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = g ∈ V ⟼ if g = ∅ ⦋ A / x⦌ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g ⦋ A / x⦌ F ⁡ g ⁡ ⋃ dom ⁡ g
18 recseq ⊢ ⦋ A / x⦌ g ∈ V ⟼ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = g ∈ V ⟼ if g = ∅ ⦋ A / x⦌ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g ⦋ A / x⦌ F ⁡ g ⁡ ⋃ dom ⁡ g → recs ⁡ ⦋ A / x⦌ g ∈ V ⟼ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = recs ⁡ g ∈ V ⟼ if g = ∅ ⦋ A / x⦌ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g ⦋ A / x⦌ F ⁡ g ⁡ ⋃ dom ⁡ g
19 17 18 syl ⊢ A ∈ V → recs ⁡ ⦋ A / x⦌ g ∈ V ⟼ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = recs ⁡ g ∈ V ⟼ if g = ∅ ⦋ A / x⦌ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g ⦋ A / x⦌ F ⁡ g ⁡ ⋃ dom ⁡ g
20 1 19 eqtrd ⊢ A ∈ V → ⦋ A / x⦌ recs ⁡ g ∈ V ⟼ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g = recs ⁡ g ∈ V ⟼ if g = ∅ ⦋ A / x⦌ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g ⦋ A / x⦌ F ⁡ g ⁡ ⋃ dom ⁡ g
21 df-rdg ⊢ rec ⁡ F I = recs ⁡ g ∈ V ⟼ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
22 21 csbeq2i ⊢ ⦋ A / x⦌ rec ⁡ F I = ⦋ A / x⦌ recs ⁡ g ∈ V ⟼ if g = ∅ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g F ⁡ g ⁡ ⋃ dom ⁡ g
23 df-rdg ⊢ rec ⁡ ⦋ A / x⦌ F ⦋ A / x⦌ I = recs ⁡ g ∈ V ⟼ if g = ∅ ⦋ A / x⦌ I if Lim ⁡ dom ⁡ g ⋃ ran ⁡ g ⦋ A / x⦌ F ⁡ g ⁡ ⋃ dom ⁡ g
24 20 22 23 3eqtr4g ⊢ A ∈ V → ⦋ A / x⦌ rec ⁡ F I = rec ⁡ ⦋ A / x⦌ F ⦋ A / x⦌ I