Metamath Proof Explorer


Theorem cdlemk40t

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

Ref Expression
Hypotheses cdlemk40.x X=ιzT|φ
cdlemk40.u U=gTifF=NgX
Assertion cdlemk40t F=NGTUG=G

Proof

Step Hyp Ref Expression
1 cdlemk40.x X=ιzT|φ
2 cdlemk40.u U=gTifF=NgX
3 1 2 cdlemk40 GTUG=ifF=NGG/gX
4 iftrue F=NifF=NGG/gX=G
5 3 4 sylan9eqr F=NGTUG=G