Metamath Proof Explorer

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 biimtrrdi ⊢ ( ( 𝐾 ∈ 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 imbitrid ⊢ ( ( 𝐾 ∈ 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 biimtrrdi ⊢ ( ( 𝐾 ∈ 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 ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑄 ) ≤ ( 𝑅 ∨ 𝑆 ) ↔ ( 𝑃 ∨ 𝑄 ) = ( 𝑅 ∨ 𝑆 ) ) )