# Metamath Proof Explorer

## Theorem cdlemk53

Description: Part of proof of Lemma K of Crawley p. 118. Line 7, p. 120. G , I stand for g, h. X represents tau. (Contributed by NM, 26-Jul-2013)

Ref Expression
Hypotheses cdlemk5.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
cdlemk5.l
cdlemk5.j
cdlemk5.m
cdlemk5.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdlemk5.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdlemk5.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
cdlemk5.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
cdlemk5.z
cdlemk5.y
cdlemk5.x ${⊢}{X}=\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({g}\right)\right)\to {z}\left({P}\right)={Y}\right)\right)$
Assertion cdlemk53

### Proof

Step Hyp Ref Expression
1 cdlemk5.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cdlemk5.l
3 cdlemk5.j
4 cdlemk5.m
5 cdlemk5.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
6 cdlemk5.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
7 cdlemk5.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
8 cdlemk5.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
9 cdlemk5.z
10 cdlemk5.y
11 cdlemk5.x ${⊢}{X}=\left(\iota {z}\in {T}|\forall {b}\in {T}\phantom{\rule{.4em}{0ex}}\left(\left({b}\ne {\mathrm{I}↾}_{{B}}\wedge {R}\left({b}\right)\ne {R}\left({F}\right)\wedge {R}\left({b}\right)\ne {R}\left({g}\right)\right)\to {z}\left({P}\right)={Y}\right)\right)$
12 simp1l
13 simp211
14 simp212
15 13 14 jca
16 simp22
17 simp213
18 simp23
19 simp1r
20 1 2 3 4 5 6 7 8 9 10 11 cdlemk35s-id
21 12 15 16 17 18 19 20 syl132anc
22 1 6 7 ltrn1o
23 12 21 22 syl2anc
24 f1of
25 fcoi1
26 23 24 25 3syl
28 simpl1l
29 13 17 19 3jca
31 simpl23
32 simpr
33 1 2 3 4 5 6 7 8 9 10 11 cdlemkid
34 28 30 31 32 33 syl112anc
35 34 coeq2d
36 32 coeq2d
37 1 6 7 ltrn1o ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {G}\in {T}\right)\to {G}:{B}\underset{1-1 onto}{⟶}{B}$
38 12 16 37 syl2anc
39 f1of ${⊢}{G}:{B}\underset{1-1 onto}{⟶}{B}\to {G}:{B}⟶{B}$
40 fcoi1 ${⊢}{G}:{B}⟶{B}\to {G}\circ \left({\mathrm{I}↾}_{{B}}\right)={G}$
41 38 39 40 3syl