Theorem dalem-cly

Description: Lemma for dalem9 . Center of perspectivity C is not in plane Y (when Y and Z are different planes). (Contributed by NM, 13-Aug-2012)

	Ref	Expression
Hypotheses	dalema.ph	$$⊢\phi \leftrightarrow \left(\left(\left(K\in \mathrm{HL}\wedge C\in {\mathrm{Base}}_K\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(Y\in O\wedge Z\in O\right)\wedge \left(\left(\neg C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }P\right)\right)\wedge \left(\neg C\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg C\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg C\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\wedge \left(C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)\wedge C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }T\right)\wedge C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\right)\right)$$
	dalemc.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dalemc.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	dalemc.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dalem-cly.o	$$⊢O=\mathrm{LPlanes}\left(K\right)$$
	dalem-cly.y	$$⊢Y=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R$$
	dalem-cly.z	$$⊢Z=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U$$
Assertion	dalem-cly	$$⊢\left(\phi \wedge Y\ne Z\right)\to \neg C\underset{\dot{}}{\le }Y$$

Proof

Step	Hyp	Ref	Expression
1		dalema.ph	$$⊢\phi \leftrightarrow \left(\left(\left(K\in \mathrm{HL}\wedge C\in {\mathrm{Base}}_K\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(Y\in O\wedge Z\in O\right)\wedge \left(\left(\neg C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }P\right)\right)\wedge \left(\neg C\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg C\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg C\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\wedge \left(C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)\wedge C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }T\right)\wedge C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\right)\right)$$
2		dalemc.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
3		dalemc.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
4		dalemc.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		dalem-cly.o	$$⊢O=\mathrm{LPlanes}\left(K\right)$$
6		dalem-cly.y	$$⊢Y=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R$$
7		dalem-cly.z	$$⊢Z=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U$$
8	1	dalemkelat	$$⊢\phi \to K\in \mathrm{Lat}$$
9	1 4	dalemceb	$$⊢\phi \to C\in {\mathrm{Base}}_K$$
10	1 5	dalemyeb	$$⊢\phi \to Y\in {\mathrm{Base}}_K$$
11		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
12	11 2 3	latleeqj1	$$⊢\left(K\in \mathrm{Lat}\wedge C\in {\mathrm{Base}}_K\wedge Y\in {\mathrm{Base}}_K\right)\to \left(C\underset{\dot{}}{\le }Y\leftrightarrow C\underset{\dot{}}{\vee }Y=Y\right)$$
13	8 9 10 12	syl3anc	$$⊢\phi \to \left(C\underset{\dot{}}{\le }Y\leftrightarrow C\underset{\dot{}}{\vee }Y=Y\right)$$
14	1	dalemclpjs	$$⊢\phi \to C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)$$
15	1	dalemkehl	$$⊢\phi \to K\in \mathrm{HL}$$
16	1 2 3 4 5 6	dalemcea	$$⊢\phi \to C\in A$$
17	1	dalemsea	$$⊢\phi \to S\in A$$
18	1	dalempea	$$⊢\phi \to P\in A$$
19	1	dalemqea	$$⊢\phi \to Q\in A$$
20	1	dalem-clpjq	$$⊢\phi \to \neg C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
21	2 3 4	atnlej1	$$⊢\left(K\in \mathrm{HL}\wedge \left(C\in A\wedge P\in A\wedge Q\in A\right)\wedge \neg C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\to C\ne P$$
22	15 16 18 19 20 21	syl131anc	$$⊢\phi \to C\ne P$$
23	2 3 4	hlatexch1	$$⊢\left(K\in \mathrm{HL}\wedge \left(C\in A\wedge S\in A\wedge P\in A\right)\wedge C\ne P\right)\to \left(C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)\to S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }C\right)\right)$$
24	15 16 17 18 22 23	syl131anc	$$⊢\phi \to \left(C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)\to S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }C\right)\right)$$
25	14 24	mpd	$$⊢\phi \to S\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }C\right)$$
26	3 4	hlatjcom	$$⊢\left(K\in \mathrm{HL}\wedge C\in A\wedge P\in A\right)\to C\underset{\dot{}}{\vee }P=P\underset{\dot{}}{\vee }C$$
27	15 16 18 26	syl3anc	$$⊢\phi \to C\underset{\dot{}}{\vee }P=P\underset{\dot{}}{\vee }C$$
28	25 27	breqtrrd	$$⊢\phi \to S\underset{\dot{}}{\le }\left(C\underset{\dot{}}{\vee }P\right)$$
29	1	dalemclqjt	$$⊢\phi \to C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }T\right)$$
30	1	dalemtea	$$⊢\phi \to T\in A$$
31	1	dalemrea	$$⊢\phi \to R\in A$$
32		simp312	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge C\in {\mathrm{Base}}_K\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(Y\in O\wedge Z\in O\right)\wedge \left(\left(\neg C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }P\right)\right)\wedge \left(\neg C\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg C\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg C\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\wedge \left(C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)\wedge C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }T\right)\wedge C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\right)\right)\to \neg C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)$$
33	1 32	sylbi	$$⊢\phi \to \neg C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)$$
34	2 3 4	atnlej1	$$⊢\left(K\in \mathrm{HL}\wedge \left(C\in A\wedge Q\in A\wedge R\in A\right)\wedge \neg C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\right)\to C\ne Q$$
35	15 16 19 31 33 34	syl131anc	$$⊢\phi \to C\ne Q$$
36	2 3 4	hlatexch1	$$⊢\left(K\in \mathrm{HL}\wedge \left(C\in A\wedge T\in A\wedge Q\in A\right)\wedge C\ne Q\right)\to \left(C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }T\right)\to T\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }C\right)\right)$$
37	15 16 30 19 35 36	syl131anc	$$⊢\phi \to \left(C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }T\right)\to T\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }C\right)\right)$$
38	29 37	mpd	$$⊢\phi \to T\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }C\right)$$
39	3 4	hlatjcom	$$⊢\left(K\in \mathrm{HL}\wedge C\in A\wedge Q\in A\right)\to C\underset{\dot{}}{\vee }Q=Q\underset{\dot{}}{\vee }C$$
40	15 16 19 39	syl3anc	$$⊢\phi \to C\underset{\dot{}}{\vee }Q=Q\underset{\dot{}}{\vee }C$$
41	38 40	breqtrrd	$$⊢\phi \to T\underset{\dot{}}{\le }\left(C\underset{\dot{}}{\vee }Q\right)$$
42	1 4	dalemseb	$$⊢\phi \to S\in {\mathrm{Base}}_K$$
43	11 3 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge C\in A\wedge P\in A\right)\to C\underset{\dot{}}{\vee }P\in {\mathrm{Base}}_K$$
44	15 16 18 43	syl3anc	$$⊢\phi \to C\underset{\dot{}}{\vee }P\in {\mathrm{Base}}_K$$
45	1 4	dalemteb	$$⊢\phi \to T\in {\mathrm{Base}}_K$$
46	11 3 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge C\in A\wedge Q\in A\right)\to C\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K$$
47	15 16 19 46	syl3anc	$$⊢\phi \to C\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K$$
48	11 2 3	latjlej12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(S\in {\mathrm{Base}}_K\wedge C\underset{\dot{}}{\vee }P\in {\mathrm{Base}}_K\right)\wedge \left(T\in {\mathrm{Base}}_K\wedge C\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\right)\right)\to \left(\left(S\underset{\dot{}}{\le }\left(C\underset{\dot{}}{\vee }P\right)\wedge T\underset{\dot{}}{\le }\left(C\underset{\dot{}}{\vee }Q\right)\right)\to \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }\left(\left(C\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\vee }\left(C\underset{\dot{}}{\vee }Q\right)\right)\right)$$
49	8 42 44 45 47 48	syl122anc	$$⊢\phi \to \left(\left(S\underset{\dot{}}{\le }\left(C\underset{\dot{}}{\vee }P\right)\wedge T\underset{\dot{}}{\le }\left(C\underset{\dot{}}{\vee }Q\right)\right)\to \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }\left(\left(C\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\vee }\left(C\underset{\dot{}}{\vee }Q\right)\right)\right)$$
50	28 41 49	mp2and	$$⊢\phi \to \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }\left(\left(C\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\vee }\left(C\underset{\dot{}}{\vee }Q\right)\right)$$
51	1 4	dalempeb	$$⊢\phi \to P\in {\mathrm{Base}}_K$$
52	1 4	dalemqeb	$$⊢\phi \to Q\in {\mathrm{Base}}_K$$
53	11 3	latjjdi	$$⊢\left(K\in \mathrm{Lat}\wedge \left(C\in {\mathrm{Base}}_K\wedge P\in {\mathrm{Base}}_K\wedge Q\in {\mathrm{Base}}_K\right)\right)\to C\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)=\left(C\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\vee }\left(C\underset{\dot{}}{\vee }Q\right)$$
54	8 9 51 52 53	syl13anc	$$⊢\phi \to C\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)=\left(C\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\vee }\left(C\underset{\dot{}}{\vee }Q\right)$$
55	50 54	breqtrrd	$$⊢\phi \to \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }\left(C\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)\right)$$
56	1	dalemclrju	$$⊢\phi \to C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)$$
57	1	dalemuea	$$⊢\phi \to U\in A$$
58		simp313	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge C\in {\mathrm{Base}}_K\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\wedge \left(Y\in O\wedge Z\in O\right)\wedge \left(\left(\neg C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }R\right)\wedge \neg C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }P\right)\right)\wedge \left(\neg C\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg C\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg C\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\wedge \left(C\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }S\right)\wedge C\underset{\dot{}}{\le }\left(Q\underset{\dot{}}{\vee }T\right)\wedge C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\right)\right)\to \neg C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }P\right)$$
59	1 58	sylbi	$$⊢\phi \to \neg C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }P\right)$$
60	2 3 4	atnlej1	$$⊢\left(K\in \mathrm{HL}\wedge \left(C\in A\wedge R\in A\wedge P\in A\right)\wedge \neg C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }P\right)\right)\to C\ne R$$
61	15 16 31 18 59 60	syl131anc	$$⊢\phi \to C\ne R$$
62	2 3 4	hlatexch1	$$⊢\left(K\in \mathrm{HL}\wedge \left(C\in A\wedge U\in A\wedge R\in A\right)\wedge C\ne R\right)\to \left(C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\to U\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }C\right)\right)$$
63	15 16 57 31 61 62	syl131anc	$$⊢\phi \to \left(C\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\to U\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }C\right)\right)$$
64	56 63	mpd	$$⊢\phi \to U\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }C\right)$$
65	3 4	hlatjcom	$$⊢\left(K\in \mathrm{HL}\wedge C\in A\wedge R\in A\right)\to C\underset{\dot{}}{\vee }R=R\underset{\dot{}}{\vee }C$$
66	15 16 31 65	syl3anc	$$⊢\phi \to C\underset{\dot{}}{\vee }R=R\underset{\dot{}}{\vee }C$$
67	64 66	breqtrrd	$$⊢\phi \to U\underset{\dot{}}{\le }\left(C\underset{\dot{}}{\vee }R\right)$$
68	1 3 4	dalemsjteb	$$⊢\phi \to S\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K$$
69	1 3 4	dalempjqeb	$$⊢\phi \to P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K$$
70	11 3	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge C\in {\mathrm{Base}}_K\wedge P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\right)\to C\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)\in {\mathrm{Base}}_K$$
71	8 9 69 70	syl3anc	$$⊢\phi \to C\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)\in {\mathrm{Base}}_K$$
72	1 4	dalemueb	$$⊢\phi \to U\in {\mathrm{Base}}_K$$
73	11 3 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge C\in A\wedge R\in A\right)\to C\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K$$
74	15 16 31 73	syl3anc	$$⊢\phi \to C\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K$$
75	11 2 3	latjlej12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(S\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K\wedge C\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)\in {\mathrm{Base}}_K\right)\wedge \left(U\in {\mathrm{Base}}_K\wedge C\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K\right)\right)\to \left(\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }\left(C\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge U\underset{\dot{}}{\le }\left(C\underset{\dot{}}{\vee }R\right)\right)\to \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }\left(\left(C\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\vee }\left(C\underset{\dot{}}{\vee }R\right)\right)\right)$$
76	8 68 71 72 74 75	syl122anc	$$⊢\phi \to \left(\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }\left(C\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)\right)\wedge U\underset{\dot{}}{\le }\left(C\underset{\dot{}}{\vee }R\right)\right)\to \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }\left(\left(C\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\vee }\left(C\underset{\dot{}}{\vee }R\right)\right)\right)$$
77	55 67 76	mp2and	$$⊢\phi \to \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }\left(\left(C\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\vee }\left(C\underset{\dot{}}{\vee }R\right)\right)$$
78	1 4	dalemreb	$$⊢\phi \to R\in {\mathrm{Base}}_K$$
79	11 3	latjjdi	$$⊢\left(K\in \mathrm{Lat}\wedge \left(C\in {\mathrm{Base}}_K\wedge P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\wedge R\in {\mathrm{Base}}_K\right)\right)\to C\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)=\left(C\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\vee }\left(C\underset{\dot{}}{\vee }R\right)$$
80	8 9 69 78 79	syl13anc	$$⊢\phi \to C\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)=\left(C\underset{\dot{}}{\vee }\left(P\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\vee }\left(C\underset{\dot{}}{\vee }R\right)$$
81	77 80	breqtrrd	$$⊢\phi \to \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }\left(C\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)$$
82	6	oveq2i	$$⊢C\underset{\dot{}}{\vee }Y=C\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
83	81 7 82	3brtr4g	$$⊢\phi \to Z\underset{\dot{}}{\le }\left(C\underset{\dot{}}{\vee }Y\right)$$
84		breq2	$$⊢C\underset{\dot{}}{\vee }Y=Y\to \left(Z\underset{\dot{}}{\le }\left(C\underset{\dot{}}{\vee }Y\right)\leftrightarrow Z\underset{\dot{}}{\le }Y\right)$$
85	83 84	syl5ibcom	$$⊢\phi \to \left(C\underset{\dot{}}{\vee }Y=Y\to Z\underset{\dot{}}{\le }Y\right)$$
86	13 85	sylbid	$$⊢\phi \to \left(C\underset{\dot{}}{\le }Y\to Z\underset{\dot{}}{\le }Y\right)$$
87	1	dalemzeo	$$⊢\phi \to Z\in O$$
88	1	dalemyeo	$$⊢\phi \to Y\in O$$
89	2 5	lplncmp	$$⊢\left(K\in \mathrm{HL}\wedge Z\in O\wedge Y\in O\right)\to \left(Z\underset{\dot{}}{\le }Y\leftrightarrow Z=Y\right)$$
90	15 87 88 89	syl3anc	$$⊢\phi \to \left(Z\underset{\dot{}}{\le }Y\leftrightarrow Z=Y\right)$$
91		eqcom	$$⊢Z=Y\leftrightarrow Y=Z$$
92	90 91	bitrdi	$$⊢\phi \to \left(Z\underset{\dot{}}{\le }Y\leftrightarrow Y=Z\right)$$
93	86 92	sylibd	$$⊢\phi \to \left(C\underset{\dot{}}{\le }Y\to Y=Z\right)$$
94	93	necon3ad	$$⊢\phi \to \left(Y\ne Z\to \neg C\underset{\dot{}}{\le }Y\right)$$
95	94	imp	$$⊢\left(\phi \wedge Y\ne Z\right)\to \neg C\underset{\dot{}}{\le }Y$$