Theorem csbfinxpg

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

	Ref	Expression
Assertion	csbfinxpg	$$⊢A\in V\to ⦋A/x⦌U\uparrow \uparrow N=⦋A/x⦌U\uparrow \uparrow ⦋A/x⦌N$$

Proof

Step	Hyp	Ref	Expression
1		df-finxp	$$⊢U\uparrow \uparrow N=\left\{y|\left(N\in \mathrm{\omega }\wedge \varnothing =\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨N,y⟩\right)\left(N\right)\right)\right\}$$
2	1	csbeq2i	$$⊢⦋A/x⦌U\uparrow \uparrow N=⦋A/x⦌\left\{y|\left(N\in \mathrm{\omega }\wedge \varnothing =\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨N,y⟩\right)\left(N\right)\right)\right\}$$
3		sbcan	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(N\in \mathrm{\omega }\wedge \varnothing =\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨N,y⟩\right)\left(N\right)\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}N\in \mathrm{\omega }\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\varnothing =\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨N,y⟩\right)\left(N\right)\right)$$
4		sbcel1g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}N\in \mathrm{\omega }\leftrightarrow ⦋A/x⦌N\in \mathrm{\omega }\right)$$
5		sbceq2g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\varnothing =\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨N,y⟩\right)\left(N\right)\leftrightarrow \varnothing =⦋A/x⦌\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨N,y⟩\right)\left(N\right)\right)$$
6		csbfv12	$$⊢⦋A/x⦌\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨N,y⟩\right)\left(N\right)=⦋A/x⦌\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨N,y⟩\right)\left(⦋A/x⦌N\right)$$
7		csbrdgg	$$⊢A\in V\to ⦋A/x⦌\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨N,y⟩\right)=\mathrm{rec}\left(⦋A/x⦌\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⦋A/x⦌⟨N,y⟩\right)$$
8		csbmpo123	$$⊢A\in V\to ⦋A/x⦌\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right)=\left(n\in ⦋A/x⦌\mathrm{\omega },z\in ⦋A/x⦌\mathrm{V}⟼⦋A/x⦌if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right)$$
9		csbconstg	$$⊢A\in V\to ⦋A/x⦌\mathrm{\omega }=\mathrm{\omega }$$
10		csbconstg	$$⊢A\in V\to ⦋A/x⦌\mathrm{V}=\mathrm{V}$$
11		csbif	$$⊢⦋A/x⦌if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)=if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(n=1_{𝑜}\wedge z\in U\right),⦋A/x⦌\varnothing ,⦋A/x⦌if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)$$
12		sbcan	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(n=1_{𝑜}\wedge z\in U\right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}n=1_{𝑜}\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in U\right)$$
13		sbcg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}n=1_{𝑜}\leftrightarrow n=1_{𝑜}\right)$$
14		sbcel12	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in U\leftrightarrow ⦋A/x⦌z\in ⦋A/x⦌U$$
15		csbconstg	$$⊢A\in V\to ⦋A/x⦌z=z$$
16	15	eleq1d	$$⊢A\in V\to \left(⦋A/x⦌z\in ⦋A/x⦌U\leftrightarrow z\in ⦋A/x⦌U\right)$$
17	14 16	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in U\leftrightarrow z\in ⦋A/x⦌U\right)$$
18	13 17	anbi12d	$$⊢A\in V\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}n=1_{𝑜}\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in U\right)\leftrightarrow \left(n=1_{𝑜}\wedge z\in ⦋A/x⦌U\right)\right)$$
19	12 18	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(n=1_{𝑜}\wedge z\in U\right)\leftrightarrow \left(n=1_{𝑜}\wedge z\in ⦋A/x⦌U\right)\right)$$
20		csbconstg	$$⊢A\in V\to ⦋A/x⦌\varnothing =\varnothing$$
21		csbif	$$⊢⦋A/x⦌if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)=if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in \left(\mathrm{V}\times U\right),⦋A/x⦌⟨\bigcup n,1^{st}\left(z\right)⟩,⦋A/x⦌⟨n,z⟩\right)$$
22		sbcel12	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in \left(\mathrm{V}\times U\right)\leftrightarrow ⦋A/x⦌z\in ⦋A/x⦌\left(\mathrm{V}\times U\right)$$
23		csbxp	$$⊢⦋A/x⦌\left(\mathrm{V}\times U\right)=⦋A/x⦌\mathrm{V}\times ⦋A/x⦌U$$
24	10	xpeq1d	$$⊢A\in V\to ⦋A/x⦌\mathrm{V}\times ⦋A/x⦌U=\mathrm{V}\times ⦋A/x⦌U$$
25	23 24	eqtrid	$$⊢A\in V\to ⦋A/x⦌\left(\mathrm{V}\times U\right)=\mathrm{V}\times ⦋A/x⦌U$$
26	15 25	eleq12d	$$⊢A\in V\to \left(⦋A/x⦌z\in ⦋A/x⦌\left(\mathrm{V}\times U\right)\leftrightarrow z\in \left(\mathrm{V}\times ⦋A/x⦌U\right)\right)$$
27	22 26	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in \left(\mathrm{V}\times U\right)\leftrightarrow z\in \left(\mathrm{V}\times ⦋A/x⦌U\right)\right)$$
28		csbconstg	$$⊢A\in V\to ⦋A/x⦌⟨\bigcup n,1^{st}\left(z\right)⟩=⟨\bigcup n,1^{st}\left(z\right)⟩$$
29		csbconstg	$$⊢A\in V\to ⦋A/x⦌⟨n,z⟩=⟨n,z⟩$$
30	27 28 29	ifbieq12d	$$⊢A\in V\to if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in \left(\mathrm{V}\times U\right),⦋A/x⦌⟨\bigcup n,1^{st}\left(z\right)⟩,⦋A/x⦌⟨n,z⟩\right)=if\left(z\in \left(\mathrm{V}\times ⦋A/x⦌U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)$$
31	21 30	eqtrid	$$⊢A\in V\to ⦋A/x⦌if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)=if\left(z\in \left(\mathrm{V}\times ⦋A/x⦌U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)$$
32	19 20 31	ifbieq12d	$$⊢A\in V\to if\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(n=1_{𝑜}\wedge z\in U\right),⦋A/x⦌\varnothing ,⦋A/x⦌if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)=if\left(\left(n=1_{𝑜}\wedge z\in ⦋A/x⦌U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times ⦋A/x⦌U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)$$
33	11 32	eqtrid	$$⊢A\in V\to ⦋A/x⦌if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)=if\left(\left(n=1_{𝑜}\wedge z\in ⦋A/x⦌U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times ⦋A/x⦌U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)$$
34	9 10 33	mpoeq123dv	$$⊢A\in V\to \left(n\in ⦋A/x⦌\mathrm{\omega },z\in ⦋A/x⦌\mathrm{V}⟼⦋A/x⦌if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right)=\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in ⦋A/x⦌U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times ⦋A/x⦌U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right)$$
35	8 34	eqtrd	$$⊢A\in V\to ⦋A/x⦌\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right)=\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in ⦋A/x⦌U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times ⦋A/x⦌U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right)$$
36		csbopg	$$⊢A\in V\to ⦋A/x⦌⟨N,y⟩=⟨⦋A/x⦌N,⦋A/x⦌y⟩$$
37		csbconstg	$$⊢A\in V\to ⦋A/x⦌y=y$$
38	37	opeq2d	$$⊢A\in V\to ⟨⦋A/x⦌N,⦋A/x⦌y⟩=⟨⦋A/x⦌N,y⟩$$
39	36 38	eqtrd	$$⊢A\in V\to ⦋A/x⦌⟨N,y⟩=⟨⦋A/x⦌N,y⟩$$
40		rdgeq12	$$⊢\left(⦋A/x⦌\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right)=\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in ⦋A/x⦌U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times ⦋A/x⦌U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right)\wedge ⦋A/x⦌⟨N,y⟩=⟨⦋A/x⦌N,y⟩\right)\to \mathrm{rec}\left(⦋A/x⦌\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⦋A/x⦌⟨N,y⟩\right)=\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in ⦋A/x⦌U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times ⦋A/x⦌U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨⦋A/x⦌N,y⟩\right)$$
41	35 39 40	syl2anc	$$⊢A\in V\to \mathrm{rec}\left(⦋A/x⦌\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⦋A/x⦌⟨N,y⟩\right)=\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in ⦋A/x⦌U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times ⦋A/x⦌U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨⦋A/x⦌N,y⟩\right)$$
42	7 41	eqtrd	$$⊢A\in V\to ⦋A/x⦌\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨N,y⟩\right)=\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in ⦋A/x⦌U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times ⦋A/x⦌U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨⦋A/x⦌N,y⟩\right)$$
43	42	fveq1d	$$⊢A\in V\to ⦋A/x⦌\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨N,y⟩\right)\left(⦋A/x⦌N\right)=\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in ⦋A/x⦌U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times ⦋A/x⦌U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨⦋A/x⦌N,y⟩\right)\left(⦋A/x⦌N\right)$$
44	6 43	eqtrid	$$⊢A\in V\to ⦋A/x⦌\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨N,y⟩\right)\left(N\right)=\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in ⦋A/x⦌U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times ⦋A/x⦌U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨⦋A/x⦌N,y⟩\right)\left(⦋A/x⦌N\right)$$
45	44	eqeq2d	$$⊢A\in V\to \left(\varnothing =⦋A/x⦌\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨N,y⟩\right)\left(N\right)\leftrightarrow \varnothing =\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in ⦋A/x⦌U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times ⦋A/x⦌U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨⦋A/x⦌N,y⟩\right)\left(⦋A/x⦌N\right)\right)$$
46	5 45	bitrd	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\varnothing =\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨N,y⟩\right)\left(N\right)\leftrightarrow \varnothing =\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in ⦋A/x⦌U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times ⦋A/x⦌U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨⦋A/x⦌N,y⟩\right)\left(⦋A/x⦌N\right)\right)$$
47	4 46	anbi12d	$$⊢A\in V\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}N\in \mathrm{\omega }\wedge \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\varnothing =\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨N,y⟩\right)\left(N\right)\right)\leftrightarrow \left(⦋A/x⦌N\in \mathrm{\omega }\wedge \varnothing =\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in ⦋A/x⦌U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times ⦋A/x⦌U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨⦋A/x⦌N,y⟩\right)\left(⦋A/x⦌N\right)\right)\right)$$
48	3 47	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(N\in \mathrm{\omega }\wedge \varnothing =\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨N,y⟩\right)\left(N\right)\right)\leftrightarrow \left(⦋A/x⦌N\in \mathrm{\omega }\wedge \varnothing =\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in ⦋A/x⦌U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times ⦋A/x⦌U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨⦋A/x⦌N,y⟩\right)\left(⦋A/x⦌N\right)\right)\right)$$
49	48	abbidv	$$⊢A\in V\to \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(N\in \mathrm{\omega }\wedge \varnothing =\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨N,y⟩\right)\left(N\right)\right)\right\}=\left\{y|\left(⦋A/x⦌N\in \mathrm{\omega }\wedge \varnothing =\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in ⦋A/x⦌U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times ⦋A/x⦌U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨⦋A/x⦌N,y⟩\right)\left(⦋A/x⦌N\right)\right)\right\}$$
50		csbab	$$⊢⦋A/x⦌\left\{y|\left(N\in \mathrm{\omega }\wedge \varnothing =\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨N,y⟩\right)\left(N\right)\right)\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\left(N\in \mathrm{\omega }\wedge \varnothing =\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨N,y⟩\right)\left(N\right)\right)\right\}$$
51		df-finxp	$$⊢⦋A/x⦌U\uparrow \uparrow ⦋A/x⦌N=\left\{y|\left(⦋A/x⦌N\in \mathrm{\omega }\wedge \varnothing =\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in ⦋A/x⦌U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times ⦋A/x⦌U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨⦋A/x⦌N,y⟩\right)\left(⦋A/x⦌N\right)\right)\right\}$$
52	49 50 51	3eqtr4g	$$⊢A\in V\to ⦋A/x⦌\left\{y|\left(N\in \mathrm{\omega }\wedge \varnothing =\mathrm{rec}\left(\left(n\in \mathrm{\omega },z\in \mathrm{V}⟼if\left(\left(n=1_{𝑜}\wedge z\in U\right),\varnothing ,if\left(z\in \left(\mathrm{V}\times U\right),⟨\bigcup n,1^{st}\left(z\right)⟩,⟨n,z⟩\right)\right)\right),⟨N,y⟩\right)\left(N\right)\right)\right\}=⦋A/x⦌U\uparrow \uparrow ⦋A/x⦌N$$
53	2 52	eqtrid	$$⊢A\in V\to ⦋A/x⦌U\uparrow \uparrow N=⦋A/x⦌U\uparrow \uparrow ⦋A/x⦌N$$