Theorem ps-1 39582

Description: The join of two atoms 𝑅 ∨ 𝑆 (specifying a projective geometry line) is determined uniquely by any two atoms (specifying two points) less than or equal to that join. Part of Lemma 16.4 of [MaedaMaeda] p. 69, showing projective space postulate PS1 in [MaedaMaeda] p. 67. (Contributed by NM, 15-Nov-2011.)

Hypotheses

Ref	Expression
ps1.l	⊢ ≤ = (le‘𝐾)
ps1.j	⊢ ∨ = (join‘𝐾)
ps1.a	⊢ 𝐴 = (Atoms‘𝐾)

Assertion

Ref	Expression
ps-1	⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆) ↔ (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑆)))

Proof of Theorem ps-1

Step	Hyp	Ref	Expression
1		oveq1 7359	. . . . . 6 ⊢ (𝑅 = 𝑃 → (𝑅 ∨ 𝑆) = (𝑃 ∨ 𝑆))
2	1	breq2d 5105	. . . . 5 ⊢ (𝑅 = 𝑃 → ((𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆) ↔ (𝑃 ∨ 𝑄) ≤ (𝑃 ∨ 𝑆)))
3	1	eqeq2d 2742	. . . . 5 ⊢ (𝑅 = 𝑃 → ((𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑆) ↔ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑆)))
4	2, 3	imbi12d 344	. . . 4 ⊢ (𝑅 = 𝑃 → (((𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆) → (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑆)) ↔ ((𝑃 ∨ 𝑄) ≤ (𝑃 ∨ 𝑆) → (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑆))))
5	4	eqcoms 2739	. . 3 ⊢ (𝑃 = 𝑅 → (((𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆) → (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑆)) ↔ ((𝑃 ∨ 𝑄) ≤ (𝑃 ∨ 𝑆) → (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑆))))
6		simp3 1138	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 ≠ 𝑅 ∧ (𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆)) → (𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆))
7		simp1 1136	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → 𝐾 ∈ HL)
8		simp21 1207	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → 𝑃 ∈ 𝐴)
9		simp3l 1202	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → 𝑅 ∈ 𝐴)
10		ps1.j	. . . . . . . . . . . . 13 ⊢ ∨ = (join‘𝐾)
11		ps1.a	. . . . . . . . . . . . 13 ⊢ 𝐴 = (Atoms‘𝐾)
12	10, 11	hlatjcom 39473	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝑃 ∨ 𝑅) = (𝑅 ∨ 𝑃))
13	7, 8, 9, 12	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → (𝑃 ∨ 𝑅) = (𝑅 ∨ 𝑃))
14	13	3ad2ant1 1133	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 ≠ 𝑅 ∧ (𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆)) → (𝑃 ∨ 𝑅) = (𝑅 ∨ 𝑃))
15		hllat 39468	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
16	15	3ad2ant1 1133	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → 𝐾 ∈ Lat)
17		eqid 2731	. . . . . . . . . . . . . . . . 17 ⊢ (Base‘𝐾) = (Base‘𝐾)
18	17, 11	atbase 39394	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ (Base‘𝐾))
19	8, 18	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → 𝑃 ∈ (Base‘𝐾))
20		simp22 1208	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → 𝑄 ∈ 𝐴)
21	17, 11	atbase 39394	. . . . . . . . . . . . . . . 16 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾))
22	20, 21	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → 𝑄 ∈ (Base‘𝐾))
23		simp3r 1203	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → 𝑆 ∈ 𝐴)
24	17, 10, 11	hlatjcl 39472	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → (𝑅 ∨ 𝑆) ∈ (Base‘𝐾))
25	7, 9, 23, 24	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → (𝑅 ∨ 𝑆) ∈ (Base‘𝐾))
26		ps1.l	. . . . . . . . . . . . . . . 16 ⊢ ≤ = (le‘𝐾)
27	17, 26, 10	latjle12 18362	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ (𝑅 ∨ 𝑆) ∈ (Base‘𝐾))) → ((𝑃 ≤ (𝑅 ∨ 𝑆) ∧ 𝑄 ≤ (𝑅 ∨ 𝑆)) ↔ (𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆)))
28	16, 19, 22, 25, 27	syl13anc 1374	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑃 ≤ (𝑅 ∨ 𝑆) ∧ 𝑄 ≤ (𝑅 ∨ 𝑆)) ↔ (𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆)))
29		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑃 ≤ (𝑅 ∨ 𝑆) ∧ 𝑄 ≤ (𝑅 ∨ 𝑆)) → 𝑃 ≤ (𝑅 ∨ 𝑆))
30	28, 29	biimtrrdi 254	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆) → 𝑃 ≤ (𝑅 ∨ 𝑆)))
31	30	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 ≠ 𝑅) → ((𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆) → 𝑃 ≤ (𝑅 ∨ 𝑆)))
32		simpl1 1192	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 ≠ 𝑅) → 𝐾 ∈ HL)
33		simpl21 1252	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 ≠ 𝑅) → 𝑃 ∈ 𝐴)
34		simpl3r 1230	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 ≠ 𝑅) → 𝑆 ∈ 𝐴)
35		simpl3l 1229	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 ≠ 𝑅) → 𝑅 ∈ 𝐴)
36		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 ≠ 𝑅) → 𝑃 ≠ 𝑅)
37	26, 10, 11	hlatexchb1 39498	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑅 ∨ 𝑆) ↔ (𝑅 ∨ 𝑃) = (𝑅 ∨ 𝑆)))
38	32, 33, 34, 35, 36, 37	syl131anc 1385	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑅 ∨ 𝑆) ↔ (𝑅 ∨ 𝑃) = (𝑅 ∨ 𝑆)))
39	31, 38	sylibd 239	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 ≠ 𝑅) → ((𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆) → (𝑅 ∨ 𝑃) = (𝑅 ∨ 𝑆)))
40	39	3impia 1117	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 ≠ 𝑅 ∧ (𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆)) → (𝑅 ∨ 𝑃) = (𝑅 ∨ 𝑆))
41	14, 40	eqtrd 2766	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 ≠ 𝑅 ∧ (𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆)) → (𝑃 ∨ 𝑅) = (𝑅 ∨ 𝑆))
42	6, 41	breqtrrd 5121	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 ≠ 𝑅 ∧ (𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆)) → (𝑃 ∨ 𝑄) ≤ (𝑃 ∨ 𝑅))
43	42	3expia 1121	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 ≠ 𝑅) → ((𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆) → (𝑃 ∨ 𝑄) ≤ (𝑃 ∨ 𝑅)))
44	17, 10, 11	hlatjcl 39472	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝑃 ∨ 𝑅) ∈ (Base‘𝐾))
45	7, 8, 9, 44	syl3anc 1373	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → (𝑃 ∨ 𝑅) ∈ (Base‘𝐾))
46	17, 26, 10	latjle12 18362	. . . . . . . . . 10 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑅) ∈ (Base‘𝐾))) → ((𝑃 ≤ (𝑃 ∨ 𝑅) ∧ 𝑄 ≤ (𝑃 ∨ 𝑅)) ↔ (𝑃 ∨ 𝑄) ≤ (𝑃 ∨ 𝑅)))
47	16, 19, 22, 45, 46	syl13anc 1374	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑃 ≤ (𝑃 ∨ 𝑅) ∧ 𝑄 ≤ (𝑃 ∨ 𝑅)) ↔ (𝑃 ∨ 𝑄) ≤ (𝑃 ∨ 𝑅)))
48		simpr 484	. . . . . . . . . 10 ⊢ ((𝑃 ≤ (𝑃 ∨ 𝑅) ∧ 𝑄 ≤ (𝑃 ∨ 𝑅)) → 𝑄 ≤ (𝑃 ∨ 𝑅))
49		simp23 1209	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → 𝑃 ≠ 𝑄)
50	49	necomd 2983	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → 𝑄 ≠ 𝑃)
51	26, 10, 11	hlatexchb1 39498	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) ∧ 𝑄 ≠ 𝑃) → (𝑄 ≤ (𝑃 ∨ 𝑅) ↔ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅)))
52	7, 20, 9, 8, 50, 51	syl131anc 1385	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → (𝑄 ≤ (𝑃 ∨ 𝑅) ↔ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅)))
53	48, 52	imbitrid 244	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑃 ≤ (𝑃 ∨ 𝑅) ∧ 𝑄 ≤ (𝑃 ∨ 𝑅)) → (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅)))
54	47, 53	sylbird 260	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ≤ (𝑃 ∨ 𝑅) → (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅)))
55	54	adantr 480	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 ≠ 𝑅) → ((𝑃 ∨ 𝑄) ≤ (𝑃 ∨ 𝑅) → (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅)))
56	43, 55	syld 47	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 ≠ 𝑅) → ((𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆) → (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅)))
57	56	3impia 1117	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 ≠ 𝑅 ∧ (𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆)) → (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅))
58	57, 41	eqtrd 2766	. . . 4 ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 ≠ 𝑅 ∧ (𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆)) → (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑆))
59	58	3expia 1121	. . 3 ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ 𝑃 ≠ 𝑅) → ((𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆) → (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑆)))
60	17, 10, 11	hlatjcl 39472	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) → (𝑃 ∨ 𝑆) ∈ (Base‘𝐾))
61	7, 8, 23, 60	syl3anc 1373	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → (𝑃 ∨ 𝑆) ∈ (Base‘𝐾))
62	17, 26, 10	latjle12 18362	. . . . . 6 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ 𝑄 ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾))) → ((𝑃 ≤ (𝑃 ∨ 𝑆) ∧ 𝑄 ≤ (𝑃 ∨ 𝑆)) ↔ (𝑃 ∨ 𝑄) ≤ (𝑃 ∨ 𝑆)))
63	16, 19, 22, 61, 62	syl13anc 1374	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑃 ≤ (𝑃 ∨ 𝑆) ∧ 𝑄 ≤ (𝑃 ∨ 𝑆)) ↔ (𝑃 ∨ 𝑄) ≤ (𝑃 ∨ 𝑆)))
64		simpr 484	. . . . 5 ⊢ ((𝑃 ≤ (𝑃 ∨ 𝑆) ∧ 𝑄 ≤ (𝑃 ∨ 𝑆)) → 𝑄 ≤ (𝑃 ∨ 𝑆))
65	63, 64	biimtrrdi 254	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ≤ (𝑃 ∨ 𝑆) → 𝑄 ≤ (𝑃 ∨ 𝑆)))
66	26, 10, 11	hlatexchb1 39498	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) ∧ 𝑄 ≠ 𝑃) → (𝑄 ≤ (𝑃 ∨ 𝑆) ↔ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑆)))
67	7, 20, 23, 8, 50, 66	syl131anc 1385	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → (𝑄 ≤ (𝑃 ∨ 𝑆) ↔ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑆)))
68	65, 67	sylibd 239	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ≤ (𝑃 ∨ 𝑆) → (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑆)))
69	5, 59, 68	pm2.61ne 3013	. 2 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆) → (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑆)))
70	17, 10, 11	hlatjcl 39472	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
71	7, 8, 20, 70	syl3anc 1373	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾))
72	17, 26	latref 18353	. . . 4 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) → (𝑃 ∨ 𝑄) ≤ (𝑃 ∨ 𝑄))
73	16, 71, 72	syl2anc 584	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → (𝑃 ∨ 𝑄) ≤ (𝑃 ∨ 𝑄))
74		breq2 5097	. . 3 ⊢ ((𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑆) → ((𝑃 ∨ 𝑄) ≤ (𝑃 ∨ 𝑄) ↔ (𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆)))
75	73, 74	syl5ibcom 245	. 2 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑆) → (𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆)))
76	69, 75	impbid 212	1 ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆) ↔ (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑆)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111   ≠ wne 2928   class class class wbr 5093  ‘cfv 6487  (class class class)co 7352  Basecbs 17126  lecple 17174  joincjn 18223  Latclat 18343  Atomscatm 39368  HLchlt 39455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5219  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-riota 7309  df-ov 7355  df-oprab 7356  df-proset 18206  df-poset 18225  df-plt 18240  df-lub 18256  df-glb 18257  df-join 18258  df-meet 18259  df-p0 18335  df-lat 18344  df-covers 39371  df-ats 39372  df-atl 39403  df-cvlat 39427  df-hlat 39456

This theorem is referenced by:  2atjlej  39584  hlatexch3N  39585  hlatexch4  39586  2llnjaN  39671  dalem1  39764  lneq2at  39883  2llnma3r  39893  cdleme11c  40366  cdleme11  40375  cdleme35a  40553  cdleme42k  40589  cdlemg8b  40733  cdlemg13a  40756  cdlemg18b  40784  cdlemg42  40834  trljco  40845