Metamath Proof Explorer


Theorem cdlemk40f

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

Ref Expression
Hypotheses cdlemk40.x 𝑋 = ( 𝑧𝑇 𝜑 )
cdlemk40.u 𝑈 = ( 𝑔𝑇 ↦ if ( 𝐹 = 𝑁 , 𝑔 , 𝑋 ) )
Assertion cdlemk40f ( ( 𝐹𝑁𝐺𝑇 ) → ( 𝑈𝐺 ) = 𝐺 / 𝑔 𝑋 )

Proof

Step Hyp Ref Expression
1 cdlemk40.x 𝑋 = ( 𝑧𝑇 𝜑 )
2 cdlemk40.u 𝑈 = ( 𝑔𝑇 ↦ if ( 𝐹 = 𝑁 , 𝑔 , 𝑋 ) )
3 1 2 cdlemk40 ( 𝐺𝑇 → ( 𝑈𝐺 ) = if ( 𝐹 = 𝑁 , 𝐺 , 𝐺 / 𝑔 𝑋 ) )
4 ifnefalse ( 𝐹𝑁 → if ( 𝐹 = 𝑁 , 𝐺 , 𝐺 / 𝑔 𝑋 ) = 𝐺 / 𝑔 𝑋 )
5 3 4 sylan9eqr ( ( 𝐹𝑁𝐺𝑇 ) → ( 𝑈𝐺 ) = 𝐺 / 𝑔 𝑋 )