Theorem ps-1

Description: The join of two atoms R .\/ S (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)

	Ref	Expression
Hypotheses	ps1.l	⊢ ≤ = ( le ‘ 𝐾 )
	ps1.j	⊢ ∨ = ( join ‘ 𝐾 )
	ps1.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion	ps-1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ↔ ( 𝑃 ∨ 𝑄 ) = ( 𝑅 ∨ 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ps1.l	⊢ ≤ = ( le ‘ 𝐾 )
2		ps1.j	⊢ ∨ = ( join ‘ 𝐾 )
3		ps1.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		oveq1	⊢ ( 𝑅 = 𝑃 → ( 𝑅 ∨ 𝑆 ) = ( 𝑃 ∨ 𝑆 ) )
5	4	breq2d	⊢ ( 𝑅 = 𝑃 → ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑃 ∨ 𝑆 ) ) )
6	4	eqeq2d	⊢ ( 𝑅 = 𝑃 → ( ( 𝑃 ∨ 𝑄 ) = ( 𝑅 ∨ 𝑆 ) ↔ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑆 ) ) )
7	5 6	imbi12d	⊢ ( 𝑅 = 𝑃 → ( ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑅 ∨ 𝑆 ) ) ↔ ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑃 ∨ 𝑆 ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑆 ) ) ) )
8	7	eqcoms	⊢ ( 𝑃 = 𝑅 → ( ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑅 ∨ 𝑆 ) ) ↔ ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑃 ∨ 𝑆 ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑆 ) ) ) )
9		simp3	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) → ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) )
10		simp1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝐾 ∈ HL )
11		simp21	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑃 ∈ 𝐴 )
12		simp3l	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑅 ∈ 𝐴 )
13	2 3	hlatjcom	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑅 ) = ( 𝑅 ∨ 𝑃 ) )
14	10 11 12 13	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑅 ) = ( 𝑅 ∨ 𝑃 ) )
15	14	3ad2ant1	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) → ( 𝑃 ∨ 𝑅 ) = ( 𝑅 ∨ 𝑃 ) )
16		hllat	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
17	16	3ad2ant1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝐾 ∈ Lat )
18		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
19	18 3	atbase	⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
20	11 19	syl	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
21		simp22	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑄 ∈ 𝐴 )
22	18 3	atbase	⊢ ( 𝑄 ∈ 𝐴 → 𝑄 ∈ ( Base ‘ 𝐾 ) )
23	21 22	syl	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
24		simp3r	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑆 ∈ 𝐴 )
25	18 2 3	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
26	10 12 24 25	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
27	18 1 2	latjle12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑅 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ≤ ( 𝑅 ∨ 𝑆 ) ∧ 𝑄 ≤ ( 𝑅 ∨ 𝑆 ) ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) )
28	17 20 23 26 27	syl13anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( 𝑃 ≤ ( 𝑅 ∨ 𝑆 ) ∧ 𝑄 ≤ ( 𝑅 ∨ 𝑆 ) ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) )
29		simpl	⊢ ( ( 𝑃 ≤ ( 𝑅 ∨ 𝑆 ) ∧ 𝑄 ≤ ( 𝑅 ∨ 𝑆 ) ) → 𝑃 ≤ ( 𝑅 ∨ 𝑆 ) )
30	28 29	syl6bir	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) → 𝑃 ≤ ( 𝑅 ∨ 𝑆 ) ) )
31	30	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑅 ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) → 𝑃 ≤ ( 𝑅 ∨ 𝑆 ) ) )
32		simpl1	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑅 ) → 𝐾 ∈ HL )
33		simpl21	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑅 ) → 𝑃 ∈ 𝐴 )
34		simpl3r	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑅 ) → 𝑆 ∈ 𝐴 )
35		simpl3l	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑅 ) → 𝑅 ∈ 𝐴 )
36		simpr	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑅 ) → 𝑃 ≠ 𝑅 )
37	1 2 3	hlatexchb1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑃 ≤ ( 𝑅 ∨ 𝑆 ) ↔ ( 𝑅 ∨ 𝑃 ) = ( 𝑅 ∨ 𝑆 ) ) )
38	32 33 34 35 36 37	syl131anc	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑅 ) → ( 𝑃 ≤ ( 𝑅 ∨ 𝑆 ) ↔ ( 𝑅 ∨ 𝑃 ) = ( 𝑅 ∨ 𝑆 ) ) )
39	31 38	sylibd	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑅 ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) → ( 𝑅 ∨ 𝑃 ) = ( 𝑅 ∨ 𝑆 ) ) )
40	39	3impia	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) → ( 𝑅 ∨ 𝑃 ) = ( 𝑅 ∨ 𝑆 ) )
41	15 40	eqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) → ( 𝑃 ∨ 𝑅 ) = ( 𝑅 ∨ 𝑆 ) )
42	9 41	breqtrrd	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) → ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑃 ∨ 𝑅 ) )
43	42	3expia	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑅 ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) → ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑃 ∨ 𝑅 ) ) )
44	18 2 3	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
45	10 11 12 44	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
46	18 1 2	latjle12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑄 ≤ ( 𝑃 ∨ 𝑅 ) ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑃 ∨ 𝑅 ) ) )
47	17 20 23 45 46	syl13anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( 𝑃 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑄 ≤ ( 𝑃 ∨ 𝑅 ) ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑃 ∨ 𝑅 ) ) )
48		simpr	⊢ ( ( 𝑃 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑄 ≤ ( 𝑃 ∨ 𝑅 ) ) → 𝑄 ≤ ( 𝑃 ∨ 𝑅 ) )
49		simp23	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑃 ≠ 𝑄 )
50	49	necomd	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → 𝑄 ≠ 𝑃 )
51	1 2 3	hlatexchb1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑄 ≠ 𝑃 ) → ( 𝑄 ≤ ( 𝑃 ∨ 𝑅 ) ↔ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) )
52	10 21 12 11 50 51	syl131anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑄 ≤ ( 𝑃 ∨ 𝑅 ) ↔ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) )
53	48 52	syl5ib	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( 𝑃 ≤ ( 𝑃 ∨ 𝑅 ) ∧ 𝑄 ≤ ( 𝑃 ∨ 𝑅 ) ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) )
54	47 53	sylbird	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑃 ∨ 𝑅 ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) )
55	54	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑅 ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑃 ∨ 𝑅 ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) )
56	43 55	syld	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑅 ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) ) )
57	56	3impia	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑅 ) )
58	57 41	eqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑅 ∧ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑅 ∨ 𝑆 ) )
59	58	3expia	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) ∧ 𝑃 ≠ 𝑅 ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑅 ∨ 𝑆 ) ) )
60	18 2 3	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
61	10 11 24 60	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
62	18 1 2	latjle12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑃 ≤ ( 𝑃 ∨ 𝑆 ) ∧ 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑃 ∨ 𝑆 ) ) )
63	17 20 23 61 62	syl13anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( 𝑃 ≤ ( 𝑃 ∨ 𝑆 ) ∧ 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑃 ∨ 𝑆 ) ) )
64		simpr	⊢ ( ( 𝑃 ≤ ( 𝑃 ∨ 𝑆 ) ∧ 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) ) → 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) )
65	63 64	syl6bir	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑃 ∨ 𝑆 ) → 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) ) )
66	1 2 3	hlatexchb1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑄 ≠ 𝑃 ) → ( 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) ↔ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑆 ) ) )
67	10 21 24 11 50 66	syl131anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑄 ≤ ( 𝑃 ∨ 𝑆 ) ↔ ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑆 ) ) )
68	65 67	sylibd	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑃 ∨ 𝑆 ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑃 ∨ 𝑆 ) ) )
69	8 59 68	pm2.61ne	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) → ( 𝑃 ∨ 𝑄 ) = ( 𝑅 ∨ 𝑆 ) ) )
70	18 2 3	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
71	10 11 21 70	syl3anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
72	18 1	latref	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑃 ∨ 𝑄 ) )
73	17 71 72	syl2anc	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑃 ∨ 𝑄 ) )
74		breq2	⊢ ( ( 𝑃 ∨ 𝑄 ) = ( 𝑅 ∨ 𝑆 ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑃 ∨ 𝑄 ) ↔ ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) )
75	73 74	syl5ibcom	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) = ( 𝑅 ∨ 𝑆 ) → ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ) )
76	69 75	impbid	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ↔ ( 𝑃 ∨ 𝑄 ) = ( 𝑅 ∨ 𝑆 ) ) )