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	bitrid	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑈 ↔ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) )
18	13 17	anbi12d	⊢ ( 𝐴 ∈ 𝑉 → ( ( [ 𝐴 / 𝑥 ] 𝑛 = 1o ∧ [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝑈 ) ↔ ( 𝑛 = 1o ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) ) )
19	12 18	bitrid	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑛 = 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	eqtrid	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( V × 𝑈 ) = ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) )
26	15 25	eleq12d	⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ ( V × 𝑈 ) ↔ 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) ) )
27	22 26	bitrid	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑧 ∈ ( V × 𝑈 ) ↔ 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) ) )
28		csbconstg	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ = ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ )
29		csbconstg	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝑛 , 𝑧 ⟩ = ⟨ 𝑛 , 𝑧 ⟩ )
30	27 28 29	ifbieq12d	⊢ ( 𝐴 ∈ 𝑉 → if ( [ 𝐴 / 𝑥 ] 𝑧 ∈ ( V × 𝑈 ) , ⦋ 𝐴 / 𝑥 ⦌ ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⦋ 𝐴 / 𝑥 ⦌ ⟨ 𝑛 , 𝑧 ⟩ ) = if ( 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) )
31	21 30	eqtrid	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) = if ( 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) )
32	19 20 31	ifbieq12d	⊢ ( 𝐴 ∈ 𝑉 → if ( [ 𝐴 / 𝑥 ] ( 𝑛 = 1o ∧ 𝑧 ∈ 𝑈 ) , ⦋ 𝐴 / 𝑥 ⦌ ∅ , ⦋ 𝐴 / 𝑥 ⦌ if ( 𝑧 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) = if ( ( 𝑛 = 1o ∧ 𝑧 ∈ ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ∅ , if ( 𝑧 ∈ ( V × ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑧 ) ⟩ , ⟨ 𝑛 , 𝑧 ⟩ ) ) )
33	11 32	eqtrid	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ 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	eqtrid	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 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	bitrid	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] ( 𝑁 ∈ ω ∧ ∅ = ( 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	eqtrid	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝑈 ↑↑ 𝑁 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝑈 ↑↑ ⦋ 𝐴 / 𝑥 ⦌ 𝑁 ) )