llncvrlpln2

Description: A lattice line under a lattice plane is covered by it. (Contributed by NM, 24-Jun-2012)

	Ref	Expression
Hypotheses	llncvrlpln2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	llncvrlpln2.c	$⊢ C = ⋖_{K}$
	llncvrlpln2.n	$⊢ N = LLines (K)$
	llncvrlpln2.p	$⊢ P = LPlanes (K)$
Assertion	llncvrlpln2	$⊢ ((K \in HL \land X \in N \land Y \in P) \land X \underset{˙}{\leq} Y) \to X C Y$

Proof

Step	Hyp	Ref	Expression
1		llncvrlpln2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		llncvrlpln2.c	$⊢ C = ⋖_{K}$
3		llncvrlpln2.n	$⊢ N = LLines (K)$
4		llncvrlpln2.p	$⊢ P = LPlanes (K)$
5		simpr	$⊢ ((K \in HL \land X \in N \land Y \in P) \land X \underset{˙}{\leq} Y) \to X \underset{˙}{\leq} Y$
6		simpl1	$⊢ ((K \in HL \land X \in N \land Y \in P) \land X \underset{˙}{\leq} Y) \to K \in HL$
7		simpl3	$⊢ ((K \in HL \land X \in N \land Y \in P) \land X \underset{˙}{\leq} Y) \to Y \in P$
8	3 4	lplnnelln	$⊢ (K \in HL \land Y \in P) \to \neg Y \in N$
9	6 7 8	syl2anc	$⊢ ((K \in HL \land X \in N \land Y \in P) \land X \underset{˙}{\leq} Y) \to \neg Y \in N$
10		simpl2	$⊢ ((K \in HL \land X \in N \land Y \in P) \land X \underset{˙}{\leq} Y) \to X \in N$
11		eleq1	$⊢ X = Y \to (X \in N \leftrightarrow Y \in N)$
12	10 11	syl5ibcom	$⊢ ((K \in HL \land X \in N \land Y \in P) \land X \underset{˙}{\leq} Y) \to (X = Y \to Y \in N)$
13	12	necon3bd	$⊢ ((K \in HL \land X \in N \land Y \in P) \land X \underset{˙}{\leq} Y) \to (\neg Y \in N \to X \neq Y)$
14	9 13	mpd	$⊢ ((K \in HL \land X \in N \land Y \in P) \land X \underset{˙}{\leq} Y) \to X \neq Y$
15		eqid	$⊢ <_{K} = <_{K}$
16	1 15	pltval	$⊢ (K \in HL \land X \in N \land Y \in P) \to (X <_{K} Y \leftrightarrow (X \underset{˙}{\leq} Y \land X \neq Y))$
17	16	adantr	$⊢ ((K \in HL \land X \in N \land Y \in P) \land X \underset{˙}{\leq} Y) \to (X <_{K} Y \leftrightarrow (X \underset{˙}{\leq} Y \land X \neq Y))$
18	5 14 17	mpbir2and	$⊢ ((K \in HL \land X \in N \land Y \in P) \land X \underset{˙}{\leq} Y) \to X <_{K} Y$
19		simpl1	$⊢ ((K \in HL \land X \in N \land Y \in P) \land X <_{K} Y) \to K \in HL$
20		simpl2	$⊢ ((K \in HL \land X \in N \land Y \in P) \land X <_{K} Y) \to X \in N$
21		eqid	$⊢ {Base}_{K} = {Base}_{K}$
22	21 3	llnbase	$⊢ X \in N \to X \in {Base}_{K}$
23	20 22	syl	$⊢ ((K \in HL \land X \in N \land Y \in P) \land X <_{K} Y) \to X \in {Base}_{K}$
24		simpl3	$⊢ ((K \in HL \land X \in N \land Y \in P) \land X <_{K} Y) \to Y \in P$
25	21 4	lplnbase	$⊢ Y \in P \to Y \in {Base}_{K}$
26	24 25	syl	$⊢ ((K \in HL \land X \in N \land Y \in P) \land X <_{K} Y) \to Y \in {Base}_{K}$
27		simpr	$⊢ ((K \in HL \land X \in N \land Y \in P) \land X <_{K} Y) \to X <_{K} Y$
28		eqid	$⊢ join (K) = join (K)$
29		eqid	$⊢ Atoms (K) = Atoms (K)$
30	21 1 15 28 2 29	hlrelat3	$⊢ ((K \in HL \land X \in {Base}_{K} \land Y \in {Base}_{K}) \land X <_{K} Y) \to \exists r \in Atoms (K) (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)$
31	19 23 26 27 30	syl31anc	$⊢ ((K \in HL \land X \in N \land Y \in P) \land X <_{K} Y) \to \exists r \in Atoms (K) (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)$
32	21 1 28 29 4	islpln2	$⊢ K \in HL \to (Y \in P \leftrightarrow (Y \in {Base}_{K} \land \exists s \in Atoms (K) \exists t \in Atoms (K) \exists u \in Atoms (K) (s \neq t \land \neg u \underset{˙}{\leq} (s join (K) t) \land Y = (s join (K) t) join (K) u)))$
33	32	adantr	$⊢ (K \in HL \land X \in N) \to (Y \in P \leftrightarrow (Y \in {Base}_{K} \land \exists s \in Atoms (K) \exists t \in Atoms (K) \exists u \in Atoms (K) (s \neq t \land \neg u \underset{˙}{\leq} (s join (K) t) \land Y = (s join (K) t) join (K) u)))$
34		simp3	$⊢ (s \neq t \land \neg u \underset{˙}{\leq} (s join (K) t) \land Y = (s join (K) t) join (K) u) \to Y = (s join (K) t) join (K) u$
35	21 28 29 3	islln2	$⊢ K \in HL \to (X \in N \leftrightarrow (X \in {Base}_{K} \land \exists p \in Atoms (K) \exists q \in Atoms (K) (p \neq q \land X = p join (K) q)))$
36		simp3l	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to X C (X join (K) r)$
37		simp3r	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to (X join (K) r) \underset{˙}{\leq} Y$
38		simp12r	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to X = p join (K) q$
39	38	oveq1d	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to X join (K) r = (p join (K) q) join (K) r$
40		simp22	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to Y = (s join (K) t) join (K) u$
41	37 39 40	3brtr3d	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to ((p join (K) q) join (K) r) \underset{˙}{\leq} ((s join (K) t) join (K) u)$
42		simp111	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to K \in HL$
43		simp112	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to p \in Atoms (K)$
44		simp113	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to q \in Atoms (K)$
45		simp23	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to r \in Atoms (K)$
46	43 44 45	3jca	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to (p \in Atoms (K) \land q \in Atoms (K) \land r \in Atoms (K))$
47		simp13l	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to s \in Atoms (K)$
48		simp13r	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to t \in Atoms (K)$
49		simp21	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to u \in Atoms (K)$
50	47 48 49	3jca	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to (s \in Atoms (K) \land t \in Atoms (K) \land u \in Atoms (K))$
51	36 38 39	3brtr3d	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to (p join (K) q) C ((p join (K) q) join (K) r)$
52	21 28 29	hlatjcl	$⊢ (K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \to p join (K) q \in {Base}_{K}$
53	42 43 44 52	syl3anc	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to p join (K) q \in {Base}_{K}$
54	21 1 28 2 29	cvr1	$⊢ (K \in HL \land p join (K) q \in {Base}_{K} \land r \in Atoms (K)) \to (\neg r \underset{˙}{\leq} (p join (K) q) \leftrightarrow (p join (K) q) C ((p join (K) q) join (K) r))$
55	42 53 45 54	syl3anc	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to (\neg r \underset{˙}{\leq} (p join (K) q) \leftrightarrow (p join (K) q) C ((p join (K) q) join (K) r))$
56	51 55	mpbird	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to \neg r \underset{˙}{\leq} (p join (K) q)$
57		simp12l	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to p \neq q$
58	1 28 29	3at	$⊢ ((K \in HL \land (p \in Atoms (K) \land q \in Atoms (K) \land r \in Atoms (K)) \land (s \in Atoms (K) \land t \in Atoms (K) \land u \in Atoms (K))) \land (\neg r \underset{˙}{\leq} (p join (K) q) \land p \neq q)) \to (((p join (K) q) join (K) r) \underset{˙}{\leq} ((s join (K) t) join (K) u) \leftrightarrow (p join (K) q) join (K) r = (s join (K) t) join (K) u)$
59	42 46 50 56 57 58	syl32anc	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to (((p join (K) q) join (K) r) \underset{˙}{\leq} ((s join (K) t) join (K) u) \leftrightarrow (p join (K) q) join (K) r = (s join (K) t) join (K) u)$
60	41 59	mpbid	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to (p join (K) q) join (K) r = (s join (K) t) join (K) u$
61	60 39 40	3eqtr4d	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to X join (K) r = Y$
62	36 61	breqtrd	$⊢ (((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \land (u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \land (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to X C Y$
63	62	3exp	$⊢ ((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \to ((u \in Atoms (K) \land Y = (s join (K) t) join (K) u \land r \in Atoms (K)) \to ((X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y) \to X C Y))$
64	63	3expd	$⊢ ((K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \land (p \neq q \land X = p join (K) q) \land (s \in Atoms (K) \land t \in Atoms (K))) \to (u \in Atoms (K) \to (Y = (s join (K) t) join (K) u \to (r \in Atoms (K) \to ((X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y) \to X C Y))))$
65	64	3exp	$⊢ (K \in HL \land p \in Atoms (K) \land q \in Atoms (K)) \to ((p \neq q \land X = p join (K) q) \to ((s \in Atoms (K) \land t \in Atoms (K)) \to (u \in Atoms (K) \to (Y = (s join (K) t) join (K) u \to (r \in Atoms (K) \to ((X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y) \to X C Y))))))$
66	65	3expib	$⊢ K \in HL \to ((p \in Atoms (K) \land q \in Atoms (K)) \to ((p \neq q \land X = p join (K) q) \to ((s \in Atoms (K) \land t \in Atoms (K)) \to (u \in Atoms (K) \to (Y = (s join (K) t) join (K) u \to (r \in Atoms (K) \to ((X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y) \to X C Y)))))))$
67	66	rexlimdvv	$⊢ K \in HL \to (\exists p \in Atoms (K) \exists q \in Atoms (K) (p \neq q \land X = p join (K) q) \to ((s \in Atoms (K) \land t \in Atoms (K)) \to (u \in Atoms (K) \to (Y = (s join (K) t) join (K) u \to (r \in Atoms (K) \to ((X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y) \to X C Y))))))$
68	67	adantld	$⊢ K \in HL \to ((X \in {Base}_{K} \land \exists p \in Atoms (K) \exists q \in Atoms (K) (p \neq q \land X = p join (K) q)) \to ((s \in Atoms (K) \land t \in Atoms (K)) \to (u \in Atoms (K) \to (Y = (s join (K) t) join (K) u \to (r \in Atoms (K) \to ((X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y) \to X C Y))))))$
69	35 68	sylbid	$⊢ K \in HL \to (X \in N \to ((s \in Atoms (K) \land t \in Atoms (K)) \to (u \in Atoms (K) \to (Y = (s join (K) t) join (K) u \to (r \in Atoms (K) \to ((X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y) \to X C Y))))))$
70	69	imp31	$⊢ ((K \in HL \land X \in N) \land (s \in Atoms (K) \land t \in Atoms (K))) \to (u \in Atoms (K) \to (Y = (s join (K) t) join (K) u \to (r \in Atoms (K) \to ((X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y) \to X C Y))))$
71	34 70	syl7	$⊢ ((K \in HL \land X \in N) \land (s \in Atoms (K) \land t \in Atoms (K))) \to (u \in Atoms (K) \to ((s \neq t \land \neg u \underset{˙}{\leq} (s join (K) t) \land Y = (s join (K) t) join (K) u) \to (r \in Atoms (K) \to ((X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y) \to X C Y))))$
72	71	rexlimdv	$⊢ ((K \in HL \land X \in N) \land (s \in Atoms (K) \land t \in Atoms (K))) \to (\exists u \in Atoms (K) (s \neq t \land \neg u \underset{˙}{\leq} (s join (K) t) \land Y = (s join (K) t) join (K) u) \to (r \in Atoms (K) \to ((X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y) \to X C Y)))$
73	72	rexlimdvva	$⊢ (K \in HL \land X \in N) \to (\exists s \in Atoms (K) \exists t \in Atoms (K) \exists u \in Atoms (K) (s \neq t \land \neg u \underset{˙}{\leq} (s join (K) t) \land Y = (s join (K) t) join (K) u) \to (r \in Atoms (K) \to ((X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y) \to X C Y)))$
74	73	adantld	$⊢ (K \in HL \land X \in N) \to ((Y \in {Base}_{K} \land \exists s \in Atoms (K) \exists t \in Atoms (K) \exists u \in Atoms (K) (s \neq t \land \neg u \underset{˙}{\leq} (s join (K) t) \land Y = (s join (K) t) join (K) u)) \to (r \in Atoms (K) \to ((X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y) \to X C Y)))$
75	33 74	sylbid	$⊢ (K \in HL \land X \in N) \to (Y \in P \to (r \in Atoms (K) \to ((X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y) \to X C Y)))$
76	75	3impia	$⊢ (K \in HL \land X \in N \land Y \in P) \to (r \in Atoms (K) \to ((X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y) \to X C Y))$
77	76	rexlimdv	$⊢ (K \in HL \land X \in N \land Y \in P) \to (\exists r \in Atoms (K) (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y) \to X C Y)$
78	77	imp	$⊢ ((K \in HL \land X \in N \land Y \in P) \land \exists r \in Atoms (K) (X C (X join (K) r) \land (X join (K) r) \underset{˙}{\leq} Y)) \to X C Y$
79	31 78	syldan	$⊢ ((K \in HL \land X \in N \land Y \in P) \land X <_{K} Y) \to X C Y$
80	18 79	syldan	$⊢ ((K \in HL \land X \in N \land Y \in P) \land X \underset{˙}{\leq} Y) \to X C Y$

Metamath Proof Explorer

Theorem llncvrlpln2

Proof