Theorem cdlemk40

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

	Ref	Expression
Hypotheses	cdlemk40.x	⊢ 𝑋 = ( ℩ 𝑧 ∈ 𝑇 𝜑 )
	cdlemk40.u	⊢ 𝑈 = ( 𝑔 ∈ 𝑇 ↦ if ( 𝐹 = 𝑁 , 𝑔 , 𝑋 ) )
Assertion	cdlemk40	⊢ ( 𝐺 ∈ 𝑇 → ( 𝑈 ‘ 𝐺 ) = if ( 𝐹 = 𝑁 , 𝐺 , ⦋ 𝐺 / 𝑔 ⦌ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		cdlemk40.x	⊢ 𝑋 = ( ℩ 𝑧 ∈ 𝑇 𝜑 )
2		cdlemk40.u	⊢ 𝑈 = ( 𝑔 ∈ 𝑇 ↦ if ( 𝐹 = 𝑁 , 𝑔 , 𝑋 ) )
3		vex	⊢ 𝑔 ∈ V
4		riotaex	⊢ ( ℩ 𝑧 ∈ 𝑇 𝜑 ) ∈ V
5	1 4	eqeltri	⊢ 𝑋 ∈ V
6	3 5	ifex	⊢ if ( 𝐹 = 𝑁 , 𝑔 , 𝑋 ) ∈ V
7	6	csbex	⊢ ⦋ 𝐺 / 𝑔 ⦌ if ( 𝐹 = 𝑁 , 𝑔 , 𝑋 ) ∈ V
8	2	fvmpts	⊢ ( ( 𝐺 ∈ 𝑇 ∧ ⦋ 𝐺 / 𝑔 ⦌ if ( 𝐹 = 𝑁 , 𝑔 , 𝑋 ) ∈ V ) → ( 𝑈 ‘ 𝐺 ) = ⦋ 𝐺 / 𝑔 ⦌ if ( 𝐹 = 𝑁 , 𝑔 , 𝑋 ) )
9	7 8	mpan2	⊢ ( 𝐺 ∈ 𝑇 → ( 𝑈 ‘ 𝐺 ) = ⦋ 𝐺 / 𝑔 ⦌ if ( 𝐹 = 𝑁 , 𝑔 , 𝑋 ) )
10		csbif	⊢ ⦋ 𝐺 / 𝑔 ⦌ if ( 𝐹 = 𝑁 , 𝑔 , 𝑋 ) = if ( [ 𝐺 / 𝑔 ] 𝐹 = 𝑁 , ⦋ 𝐺 / 𝑔 ⦌ 𝑔 , ⦋ 𝐺 / 𝑔 ⦌ 𝑋 )
11		sbcg	⊢ ( 𝐺 ∈ 𝑇 → ( [ 𝐺 / 𝑔 ] 𝐹 = 𝑁 ↔ 𝐹 = 𝑁 ) )
12		csbvarg	⊢ ( 𝐺 ∈ 𝑇 → ⦋ 𝐺 / 𝑔 ⦌ 𝑔 = 𝐺 )
13	11 12	ifbieq1d	⊢ ( 𝐺 ∈ 𝑇 → if ( [ 𝐺 / 𝑔 ] 𝐹 = 𝑁 , ⦋ 𝐺 / 𝑔 ⦌ 𝑔 , ⦋ 𝐺 / 𝑔 ⦌ 𝑋 ) = if ( 𝐹 = 𝑁 , 𝐺 , ⦋ 𝐺 / 𝑔 ⦌ 𝑋 ) )
14	10 13	syl5eq	⊢ ( 𝐺 ∈ 𝑇 → ⦋ 𝐺 / 𝑔 ⦌ if ( 𝐹 = 𝑁 , 𝑔 , 𝑋 ) = if ( 𝐹 = 𝑁 , 𝐺 , ⦋ 𝐺 / 𝑔 ⦌ 𝑋 ) )
15	9 14	eqtrd	⊢ ( 𝐺 ∈ 𝑇 → ( 𝑈 ‘ 𝐺 ) = if ( 𝐹 = 𝑁 , 𝐺 , ⦋ 𝐺 / 𝑔 ⦌ 𝑋 ) )