# Metamath Proof Explorer

## Theorem cdleme39n

Description: Part of proof of Lemma E in Crawley p. 113. Show that f(x) is one-to-one on P .\/ Q line. TODO: FIX COMMENT. E , Y , G , Z serve as f(t), f(u), f_t( R ), f_t( S ). Put hypotheses of cdleme38n in convention of cdleme32sn1awN . TODO see if this hypothesis conversion would be better if done earlier. (Contributed by NM, 15-Mar-2013)

Ref Expression
Hypotheses cdleme39.l
cdleme39.j
cdleme39.m
cdleme39.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdleme39.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdleme39.u
cdleme39.e
cdleme39.g
cdleme39.y
cdleme39.z
Assertion cdleme39n

### Proof

Step Hyp Ref Expression
1 cdleme39.l
2 cdleme39.j
3 cdleme39.m
4 cdleme39.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
5 cdleme39.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
6 cdleme39.u
7 cdleme39.e
8 cdleme39.g
9 cdleme39.y
10 cdleme39.z
11 eqid
12 eqid
13 eqid
14 eqid
15 1 2 3 4 5 6 7 9 11 12 13 14 cdleme38n
16 simp11
17 simp12l
18 simp13l
19 simp22l
20 simp22r
21 simp311
22 simp32l
23 1 2 3 4 5 6 7 8 11 cdleme39a
24 16 17 18 19 20 21 22 23 syl322anc
25 simp23l
26 simp23r
27 simp312
28 simp33l
29 1 2 3 4 5 6 9 10 12 cdleme39a
30 16 17 18 25 26 27 28 29 syl322anc
31 15 24 30 3netr4d