Theorem cdlemk40

Description: TODO: fix comment. (Contributed by NM, 31-Jul-2013)

	Ref	Expression
Hypotheses	cdlemk40.x	$$⊢X=\left(\iota z\in T|\phi \right)$$
	cdlemk40.u	$$⊢U=\left(g\in T⟼if\left(F=N,g,X\right)\right)$$
Assertion	cdlemk40	$$⊢G\in T\to U\left(G\right)=if\left(F=N,G,⦋G/g⦌X\right)$$

Proof

Step	Hyp	Ref	Expression
1		cdlemk40.x	$$⊢X=\left(\iota z\in T|\phi \right)$$
2		cdlemk40.u	$$⊢U=\left(g\in T⟼if\left(F=N,g,X\right)\right)$$
3		vex	$$⊢g\in \mathrm{V}$$
4		riotaex	$$⊢\left(\iota z\in T|\phi \right)\in \mathrm{V}$$
5	1 4	eqeltri	$$⊢X\in \mathrm{V}$$
6	3 5	ifex	$$⊢if\left(F=N,g,X\right)\in \mathrm{V}$$
7	6	csbex	$$⊢⦋G/g⦌if\left(F=N,g,X\right)\in \mathrm{V}$$
8	2	fvmpts	$$⊢\left(G\in T\wedge ⦋G/g⦌if\left(F=N,g,X\right)\in \mathrm{V}\right)\to U\left(G\right)=⦋G/g⦌if\left(F=N,g,X\right)$$
9	7 8	mpan2	$$⊢G\in T\to U\left(G\right)=⦋G/g⦌if\left(F=N,g,X\right)$$
10		csbif	$$⊢⦋G/g⦌if\left(F=N,g,X\right)=if\left(\underset{\dot{}}{[}G/g\underset{\dot{}}{]}F=N,⦋G/g⦌g,⦋G/g⦌X\right)$$
11		sbcg	$$⊢G\in T\to \left(\underset{\dot{}}{[}G/g\underset{\dot{}}{]}F=N\leftrightarrow F=N\right)$$
12		csbvarg	$$⊢G\in T\to ⦋G/g⦌g=G$$
13	11 12	ifbieq1d	$$⊢G\in T\to if\left(\underset{\dot{}}{[}G/g\underset{\dot{}}{]}F=N,⦋G/g⦌g,⦋G/g⦌X\right)=if\left(F=N,G,⦋G/g⦌X\right)$$
14	10 13	syl5eq	$$⊢G\in T\to ⦋G/g⦌if\left(F=N,g,X\right)=if\left(F=N,G,⦋G/g⦌X\right)$$
15	9 14	eqtrd	$$⊢G\in T\to U\left(G\right)=if\left(F=N,G,⦋G/g⦌X\right)$$