Metamath Proof Explorer

Theorem csbfinxpg

Description: Distribute proper substitution through Cartesian exponentiation. (Contributed by ML, 25-Oct-2020)

Ref Expression
Assertion csbfinxpg ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝑈 ↑↑ 𝑁 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ↑↑ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 df-finxp ⊢ ( 𝑈 ↑↑ 𝑁 ) = { 𝑦 ∣ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) }
2 1 csbeq2i ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝑈 ↑↑ 𝑁 ) = ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) }
3 sbcan ⊢ ( [ 𝐴 / 𝑥 ] ( 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) ↔ ( [ 𝐴 / 𝑥 ] 𝑁 ∈ ω ∧ [ 𝐴 / 𝑥 ] ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) )
4 sbcel1g ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑁 ∈ ω ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 ∈ ω ) )
5 sbceq2g ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ↔ ∅ = ⦋ 𝐴 / 𝑥 ⦌ ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) )
6 csbfv12 ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) = ( ⦋ 𝐴 / 𝑥 ⦌ rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 )
7 csbrdgg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) = rec ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝑁 , 𝑦 ⟩ ) )
8 csbmpo123 ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) = ( 𝑛 ∈ ⦋ 𝐴 / 𝑥 ⦌ ω , 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ V ↦ ⦋ 𝐴 / 𝑥 ⦌ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) )
9 csbconstg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ω = ω )
10 csbconstg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ V = V )
11 csbif ⊢ ⦋ 𝐴 / 𝑥 ⦌ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) = if ( [ 𝐴 / 𝑥 ] ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ⦋ 𝐴 / 𝑥 ⦌ ∅ , ⦋ 𝐴 / 𝑥 ⦌ if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) )
12 sbcan ⊢ ( [ 𝐴 / 𝑥 ] ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) ↔ ( [ 𝐴 / 𝑥 ] 𝑛 = 1o ∧ [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑈 ) )
13 sbcg ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑛 = 1o ↔ 𝑛 = 1o ) )
14 sbcel12 ⊢ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑈 ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 )
15 csbconstg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 𝑧 = 𝑧 )
16 15 eleq1d ⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ↔ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) )
17 14 16 syl5bb ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑈 ↔ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) )
18 13 17 anbi12d ⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] 𝑛 = 1o ∧ [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑈 ) ↔ ( 𝑛 = 1o ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) ) )
19 12 18 syl5bb ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) ↔ ( 𝑛 = 1o ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) ) )
20 csbconstg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ∅ = ∅ )
21 csbif ⊢ ⦋ 𝐴 / 𝑥 ⦌ if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) = if ( [ 𝐴 / 𝑥 ] 𝑧 ∈ ( V × 𝑈 ) , ⦋ 𝐴 / 𝑥 ⦌ ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝑛 , 𝑧 ⟩ )
22 sbcel12 ⊢ ( [ 𝐴 / 𝑥 ] 𝑧 ∈ ( V × 𝑈 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ ( V × 𝑈 ) )
23 csbxp ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( V × 𝑈 ) = ( ⦋ 𝐴 / 𝑥 ⦌ V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 )
24 10 xpeq1d ⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) = ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) )
25 23 24 syl5eq ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( V × 𝑈 ) = ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) )
26 15 25 eleq12d ⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ ( V × 𝑈 ) ↔ 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) ) )
27 22 26 syl5bb ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑧 ∈ ( V × 𝑈 ) ↔ 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) ) )
28 csbconstg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ = ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ )
29 csbconstg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝑛 , 𝑧 ⟩ = ⟨ 𝑛 , 𝑧 ⟩ )
30 27 28 29 ifbieq12d ⊢ ( 𝐴 ∈ 𝑉 → if ( [ 𝐴 / 𝑥 ] 𝑧 ∈ ( V × 𝑈 ) , ⦋ 𝐴 / 𝑥 ⦌ ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝑛 , 𝑧 ⟩ ) = if ( 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) )
31 21 30 syl5eq ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) = if ( 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) )
32 19 20 31 ifbieq12d ⊢ ( 𝐴 ∈ 𝑉 → if ( [ 𝐴 / 𝑥 ] ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ⦋ 𝐴 / 𝑥 ⦌ ∅ , ⦋ 𝐴 / 𝑥 ⦌ if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) = if ( ( 𝑛 = 1o ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) )
33 11 32 syl5eq ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) = if ( ( 𝑛 = 1o ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) )
34 9 10 33 mpoeq123dv ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑛 ∈ ⦋ 𝐴 / 𝑥 ⦌ ω , 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ V ↦ ⦋ 𝐴 / 𝑥 ⦌ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) = ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) )
35 8 34 eqtrd ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) = ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) )
36 csbopg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝑁 , 𝑦 ⟩ = ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 , ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ⟩ )
37 csbconstg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 𝑦 = 𝑦 )
38 37 opeq2d ⊢ ( 𝐴 ∈ 𝑉 → ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 , ⦋ 𝐴 / 𝑥 ⦌ 𝑦 ⟩ = ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 , 𝑦 ⟩ )
39 36 38 eqtrd ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝑁 , 𝑦 ⟩ = ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 , 𝑦 ⟩ )
40 rdgeq12 ⊢ ( ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) = ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) ∧ ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝑁 , 𝑦 ⟩ = ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 , 𝑦 ⟩ ) → rec ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝑁 , 𝑦 ⟩ ) = rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 , 𝑦 ⟩ ) )
41 35 39 40 syl2anc ⊢ ( 𝐴 ∈ 𝑉 → rec ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝑁 , 𝑦 ⟩ ) = rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 , 𝑦 ⟩ ) )
42 7 41 eqtrd ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) = rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 , 𝑦 ⟩ ) )
43 42 fveq1d ⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 ) = ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 , 𝑦 ⟩ ) ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 ) )
44 6 43 syl5eq ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) = ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 , 𝑦 ⟩ ) ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 ) )
45 44 eqeq2d ⊢ ( 𝐴 ∈ 𝑉 → ( ∅ = ⦋ 𝐴 / 𝑥 ⦌ ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ↔ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 , 𝑦 ⟩ ) ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 ) ) )
46 5 45 bitrd ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ↔ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 , 𝑦 ⟩ ) ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 ) ) )
47 4 46 anbi12d ⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] 𝑁 ∈ ω ∧ [ 𝐴 / 𝑥 ] ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 , 𝑦 ⟩ ) ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 ) ) ) )
48 3 47 syl5bb ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) ↔ ( ⦋ 𝐴 / 𝑥 ⦌ 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 , 𝑦 ⟩ ) ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 ) ) ) )
49 48 abbidv ⊢ ( 𝐴 ∈ 𝑉 → { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) } = { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 , 𝑦 ⟩ ) ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 ) ) } )
50 csbab ⊢ ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) } = { 𝑦 ∣ [ 𝐴 / 𝑥 ] ( 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) }
51 df-finxp ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ↑↑ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 ) = { 𝑦 ∣ ( ⦋ 𝐴 / 𝑥 ⦌ 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 , 𝑦 ⟩ ) ‘ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 ) ) }
52 49 50 51 3eqtr4g ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { 𝑦 ∣ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑧 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) } = ( ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ↑↑ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 ) )
53 2 52 syl5eq ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝑈 ↑↑ 𝑁 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ↑↑ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 ) )