Metamath Proof Explorer

Theorem cvlcvr1

Description: The covering property. Proposition 1(ii) in Kalmbach p. 140 (and its converse). ( chcv1 analog.) (Contributed by NM, 5-Nov-2012)

Ref Expression
Hypotheses cvlcvr1.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cvlcvr1.l ⊢ ≤ = ( le ‘ 𝐾 )
cvlcvr1.j ⊢ ∨ = ( join ‘ 𝐾 )
cvlcvr1.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
cvlcvr1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion cvlcvr1 ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ¬ 𝑃 ≤ 𝑋 ↔ 𝑋 𝐶 ( 𝑋 ∨ 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 cvlcvr1.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cvlcvr1.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cvlcvr1.j ⊢ ∨ = ( join ‘ 𝐾 )
4 cvlcvr1.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
5 cvlcvr1.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6 simp13 ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → 𝐾 ∈ CvLat )
7 cvllat ⊢ ( 𝐾 ∈ CvLat → 𝐾 ∈ Lat )
8 6 7 syl ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → 𝐾 ∈ Lat )
9 simp2 ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
10 1 5 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵 )
11 10 3ad2ant3 ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ∈ 𝐵 )
12 eqid ⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
13 1 2 12 3 latnle ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐵 ) → ( ¬ 𝑃 ≤ 𝑋 ↔ 𝑋 ( lt ‘ 𝐾 ) ( 𝑋 ∨ 𝑃 ) ) )
14 8 9 11 13 syl3anc ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ¬ 𝑃 ≤ 𝑋 ↔ 𝑋 ( lt ‘ 𝐾 ) ( 𝑋 ∨ 𝑃 ) ) )
15 14 biimpd ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ¬ 𝑃 ≤ 𝑋 → 𝑋 ( lt ‘ 𝐾 ) ( 𝑋 ∨ 𝑃 ) ) )
16 simpl13 ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) → 𝐾 ∈ CvLat )
17 16 7 syl ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) → 𝐾 ∈ Lat )
18 simprll ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) → 𝑧 ∈ 𝐵 )
19 simpl2 ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) → 𝑋 ∈ 𝐵 )
20 simpl3 ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) → 𝑃 ∈ 𝐴 )
21 20 10 syl ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) → 𝑃 ∈ 𝐵 )
22 1 3 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑃 ) ∈ 𝐵 )
23 17 19 21 22 syl3anc ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) → ( 𝑋 ∨ 𝑃 ) ∈ 𝐵 )
24 simprrr ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) → 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) )
25 simprrl ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) → 𝑋 ( lt ‘ 𝐾 ) 𝑧 )
26 simpl11 ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) → 𝐾 ∈ OML )
27 simpl12 ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) → 𝐾 ∈ CLat )
28 cvlatl ⊢ ( 𝐾 ∈ CvLat → 𝐾 ∈ AtLat )
29 16 28 syl ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) → 𝐾 ∈ AtLat )
30 1 2 12 5 atlrelat1 ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 → ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) ) )
31 26 27 29 19 18 30 syl311anc ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 → ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) ) )
32 25 31 mpd ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) → ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) )
33 17 adantr ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) ) ) → 𝐾 ∈ Lat )
34 1 5 atbase ⊢ ( 𝑞 ∈ 𝐴 → 𝑞 ∈ 𝐵 )
35 34 ad2antrl ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) ) ) → 𝑞 ∈ 𝐵 )
36 18 adantr ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) ) ) → 𝑧 ∈ 𝐵 )
37 23 adantr ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) ) ) → ( 𝑋 ∨ 𝑃 ) ∈ 𝐵 )
38 simprrr ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) ) ) → 𝑞 ≤ 𝑧 )
39 24 adantr ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) ) ) → 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) )
40 1 2 33 35 36 37 38 39 lattrd ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) ) ) → 𝑞 ≤ ( 𝑋 ∨ 𝑃 ) )
41 16 adantr ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) ) ) → 𝐾 ∈ CvLat )
42 simprl ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) ) ) → 𝑞 ∈ 𝐴 )
43 simpll3 ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) ) ) → 𝑃 ∈ 𝐴 )
44 simpll2 ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) ) ) → 𝑋 ∈ 𝐵 )
45 simprrl ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) ) ) → ¬ 𝑞 ≤ 𝑋 )
46 1 2 3 5 cvlexch1 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑞 ≤ 𝑋 ) → ( 𝑞 ≤ ( 𝑋 ∨ 𝑃 ) → 𝑃 ≤ ( 𝑋 ∨ 𝑞 ) ) )
47 41 42 43 44 45 46 syl131anc ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) ) ) → ( 𝑞 ≤ ( 𝑋 ∨ 𝑃 ) → 𝑃 ≤ ( 𝑋 ∨ 𝑞 ) ) )
48 40 47 mpd ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) ) ) → 𝑃 ≤ ( 𝑋 ∨ 𝑞 ) )
49 simprlr ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) → ¬ 𝑃 ≤ 𝑋 )
50 49 adantr ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) ) ) → ¬ 𝑃 ≤ 𝑋 )
51 1 2 3 5 cvlexchb1 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) ∧ ¬ 𝑃 ≤ 𝑋 ) → ( 𝑃 ≤ ( 𝑋 ∨ 𝑞 ) ↔ ( 𝑋 ∨ 𝑃 ) = ( 𝑋 ∨ 𝑞 ) ) )
52 41 43 42 44 50 51 syl131anc ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) ) ) → ( 𝑃 ≤ ( 𝑋 ∨ 𝑞 ) ↔ ( 𝑋 ∨ 𝑃 ) = ( 𝑋 ∨ 𝑞 ) ) )
53 48 52 mpbid ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) ) ) → ( 𝑋 ∨ 𝑃 ) = ( 𝑋 ∨ 𝑞 ) )
54 2 12 pltle ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 → 𝑋 ≤ 𝑧 ) )
55 26 19 18 54 syl3anc ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) → ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 → 𝑋 ≤ 𝑧 ) )
56 25 55 mpd ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) → 𝑋 ≤ 𝑧 )
57 56 adantr ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) ) ) → 𝑋 ≤ 𝑧 )
58 1 2 3 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑋 ≤ 𝑧 ∧ 𝑞 ≤ 𝑧 ) ↔ ( 𝑋 ∨ 𝑞 ) ≤ 𝑧 ) )
59 33 44 35 36 58 syl13anc ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) ) ) → ( ( 𝑋 ≤ 𝑧 ∧ 𝑞 ≤ 𝑧 ) ↔ ( 𝑋 ∨ 𝑞 ) ≤ 𝑧 ) )
60 57 38 59 mpbi2and ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) ) ) → ( 𝑋 ∨ 𝑞 ) ≤ 𝑧 )
61 53 60 eqbrtrd ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) ∧ ( 𝑞 ∈ 𝐴 ∧ ( ¬ 𝑞 ≤ 𝑋 ∧ 𝑞 ≤ 𝑧 ) ) ) → ( 𝑋 ∨ 𝑃 ) ≤ 𝑧 )
62 32 61 rexlimddv ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) → ( 𝑋 ∨ 𝑃 ) ≤ 𝑧 )
63 1 2 17 18 23 24 62 latasymd ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑧 ∈ 𝐵 ∧ ¬ 𝑃 ≤ 𝑋 ) ∧ ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) ) ) → 𝑧 = ( 𝑋 ∨ 𝑃 ) )
64 63 exp44 ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑧 ∈ 𝐵 → ( ¬ 𝑃 ≤ 𝑋 → ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) → 𝑧 = ( 𝑋 ∨ 𝑃 ) ) ) ) )
65 64 imp ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐵 ) → ( ¬ 𝑃 ≤ 𝑋 → ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) → 𝑧 = ( 𝑋 ∨ 𝑃 ) ) ) )
66 65 ralrimdva ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ¬ 𝑃 ≤ 𝑋 → ∀ 𝑧 ∈ 𝐵 ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) → 𝑧 = ( 𝑋 ∨ 𝑃 ) ) ) )
67 15 66 jcad ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ¬ 𝑃 ≤ 𝑋 → ( 𝑋 ( lt ‘ 𝐾 ) ( 𝑋 ∨ 𝑃 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) → 𝑧 = ( 𝑋 ∨ 𝑃 ) ) ) ) )
68 8 9 11 22 syl3anc ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑋 ∨ 𝑃 ) ∈ 𝐵 )
69 1 2 12 4 cvrval2 ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑃 ) ∈ 𝐵 ) → ( 𝑋 𝐶 ( 𝑋 ∨ 𝑃 ) ↔ ( 𝑋 ( lt ‘ 𝐾 ) ( 𝑋 ∨ 𝑃 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) → 𝑧 = ( 𝑋 ∨ 𝑃 ) ) ) ) )
70 8 9 68 69 syl3anc ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑋 𝐶 ( 𝑋 ∨ 𝑃 ) ↔ ( 𝑋 ( lt ‘ 𝐾 ) ( 𝑋 ∨ 𝑃 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑧 ∧ 𝑧 ≤ ( 𝑋 ∨ 𝑃 ) ) → 𝑧 = ( 𝑋 ∨ 𝑃 ) ) ) ) )
71 67 70 sylibrd ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ¬ 𝑃 ≤ 𝑋 → 𝑋 𝐶 ( 𝑋 ∨ 𝑃 ) ) )
72 8 adantr ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑋 𝐶 ( 𝑋 ∨ 𝑃 ) ) → 𝐾 ∈ Lat )
73 simpl2 ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑋 𝐶 ( 𝑋 ∨ 𝑃 ) ) → 𝑋 ∈ 𝐵 )
74 68 adantr ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑋 𝐶 ( 𝑋 ∨ 𝑃 ) ) → ( 𝑋 ∨ 𝑃 ) ∈ 𝐵 )
75 simpr ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑋 𝐶 ( 𝑋 ∨ 𝑃 ) ) → 𝑋 𝐶 ( 𝑋 ∨ 𝑃 ) )
76 1 12 4 cvrlt ⊢ ( ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑃 ) ∈ 𝐵 ) ∧ 𝑋 𝐶 ( 𝑋 ∨ 𝑃 ) ) → 𝑋 ( lt ‘ 𝐾 ) ( 𝑋 ∨ 𝑃 ) )
77 72 73 74 75 76 syl31anc ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑋 𝐶 ( 𝑋 ∨ 𝑃 ) ) → 𝑋 ( lt ‘ 𝐾 ) ( 𝑋 ∨ 𝑃 ) )
78 77 ex ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑋 𝐶 ( 𝑋 ∨ 𝑃 ) → 𝑋 ( lt ‘ 𝐾 ) ( 𝑋 ∨ 𝑃 ) ) )
79 78 14 sylibrd ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑋 𝐶 ( 𝑋 ∨ 𝑃 ) → ¬ 𝑃 ≤ 𝑋 ) )
80 71 79 impbid ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat ) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ) → ( ¬ 𝑃 ≤ 𝑋 ↔ 𝑋 𝐶 ( 𝑋 ∨ 𝑃 ) ) )