Metamath Proof Explorer

Theorem atlatmstc

Description: An atomic, complete, orthomodular lattice is atomistic i.e. every element is the join of the atoms under it. See remark before Proposition 1 in Kalmbach p. 140; also remark in BeltramettiCassinelli p. 98. ( hatomistici analog.) (Contributed by NM, 5-Nov-2012)

Ref Expression
Hypotheses atlatmstc.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
atlatmstc.l ⊢ ≤ = ( le ‘ 𝐾 )
atlatmstc.u ⊢ 1 = ( lub ‘ 𝐾 )
atlatmstc.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion atlatmstc ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 atlatmstc.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 atlatmstc.l ⊢ ≤ = ( le ‘ 𝐾 )
3 atlatmstc.u ⊢ 1 = ( lub ‘ 𝐾 )
4 atlatmstc.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5 simpl2 ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ CLat )
6 ssrab2 ⊢ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } ⊆ 𝐵
7 1 4 atssbase ⊢ 𝐴 ⊆ 𝐵
8 rabss2 ⊢ ( 𝐴 ⊆ 𝐵 → { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ⊆ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } )
9 7 8 ax-mp ⊢ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ⊆ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 }
10 1 2 3 lubss ⊢ ( ( 𝐾 ∈ CLat ∧ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } ⊆ 𝐵 ∧ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ⊆ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } ) → ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ≤ ( 1 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } ) )
11 6 9 10 mp3an23 ⊢ ( 𝐾 ∈ CLat → ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ≤ ( 1 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } ) )
12 5 11 syl ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ≤ ( 1 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } ) )
13 atlpos ⊢ ( 𝐾 ∈ AtLat → 𝐾 ∈ Poset )
14 13 3ad2ant3 ⊢ ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) → 𝐾 ∈ Poset )
15 simpl ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ Poset )
16 simpr ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
17 1 2 3 15 16 lubid ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ) → ( 1 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } ) = 𝑋 )
18 14 17 sylan ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → ( 1 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } ) = 𝑋 )
19 12 18 breqtrd ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ≤ 𝑋 )
20 breq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ≤ 𝑋 ↔ 𝑥 ≤ 𝑋 ) )
21 20 elrab ⊢ ( 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑋 ) )
22 simpll2 ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) → 𝐾 ∈ CLat )
23 ssrab2 ⊢ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ⊆ 𝐴
24 23 7 sstri ⊢ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ⊆ 𝐵
25 1 2 3 lubel ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ∧ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ⊆ 𝐵 ) → 𝑥 ≤ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) )
26 24 25 mp3an3 ⊢ ( ( 𝐾 ∈ CLat ∧ 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) → 𝑥 ≤ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) )
27 22 26 sylancom ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) → 𝑥 ≤ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) )
28 27 ex ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } → 𝑥 ≤ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) )
29 21 28 syl5bir ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑋 ) → 𝑥 ≤ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) )
30 29 expdimp ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ≤ 𝑋 → 𝑥 ≤ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) )
31 simpll3 ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐾 ∈ AtLat )
32 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
33 32 4 atn0 ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≠ ( 0. ‘ 𝐾 ) )
34 31 33 sylancom ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≠ ( 0. ‘ 𝐾 ) )
35 34 adantr ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 ≤ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) → 𝑥 ≠ ( 0. ‘ 𝐾 ) )
36 simpl3 ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ AtLat )
37 atllat ⊢ ( 𝐾 ∈ AtLat → 𝐾 ∈ Lat )
38 36 37 syl ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ Lat )
39 38 adantr ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝐾 ∈ Lat )
40 1 4 atbase ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 )
41 40 adantl ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
42 1 3 clatlubcl ⊢ ( ( 𝐾 ∈ CLat ∧ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ⊆ 𝐵 ) → ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ∈ 𝐵 )
43 5 24 42 sylancl ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ∈ 𝐵 )
44 43 adantr ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ∈ 𝐵 )
45 simpl1 ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ OML )
46 omlop ⊢ ( 𝐾 ∈ OML → 𝐾 ∈ OP )
47 45 46 syl ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → 𝐾 ∈ OP )
48 eqid ⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
49 1 48 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ∈ 𝐵 )
50 47 43 49 syl2anc ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ∈ 𝐵 )
51 50 adantr ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ∈ 𝐵 )
52 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
53 1 2 52 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ∈ 𝐵 ) ) → ( ( 𝑥 ≤ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ∧ 𝑥 ≤ ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ↔ 𝑥 ≤ ( ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ) )
54 39 41 44 51 53 syl13anc ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ≤ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ∧ 𝑥 ≤ ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ↔ 𝑥 ≤ ( ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ) )
55 1 48 52 32 opnoncon ⊢ ( ( 𝐾 ∈ OP ∧ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ∈ 𝐵 ) → ( ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) = ( 0. ‘ 𝐾 ) )
56 47 43 55 syl2anc ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → ( ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) = ( 0. ‘ 𝐾 ) )
57 56 breq2d ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝑥 ≤ ( ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ↔ 𝑥 ≤ ( 0. ‘ 𝐾 ) ) )
58 57 adantr ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ≤ ( ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ↔ 𝑥 ≤ ( 0. ‘ 𝐾 ) ) )
59 1 2 32 ople0 ⊢ ( ( 𝐾 ∈ OP ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ≤ ( 0. ‘ 𝐾 ) ↔ 𝑥 = ( 0. ‘ 𝐾 ) ) )
60 47 40 59 syl2an ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ≤ ( 0. ‘ 𝐾 ) ↔ 𝑥 = ( 0. ‘ 𝐾 ) ) )
61 54 58 60 3bitrd ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ≤ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ∧ 𝑥 ≤ ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ↔ 𝑥 = ( 0. ‘ 𝐾 ) ) )
62 61 biimpa ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑥 ≤ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ∧ 𝑥 ≤ ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ) → 𝑥 = ( 0. ‘ 𝐾 ) )
63 62 expr ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 ≤ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) → ( 𝑥 ≤ ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) → 𝑥 = ( 0. ‘ 𝐾 ) ) )
64 63 necon3ad ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 ≤ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) → ( 𝑥 ≠ ( 0. ‘ 𝐾 ) → ¬ 𝑥 ≤ ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) )
65 35 64 mpd ⊢ ( ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 ≤ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) → ¬ 𝑥 ≤ ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) )
66 65 ex ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ≤ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) → ¬ 𝑥 ≤ ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) )
67 30 66 syld ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ≤ 𝑋 → ¬ 𝑥 ≤ ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) )
68 imnan ⊢ ( ( 𝑥 ≤ 𝑋 → ¬ 𝑥 ≤ ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ↔ ¬ ( 𝑥 ≤ 𝑋 ∧ 𝑥 ≤ ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) )
69 67 68 sylib ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ¬ ( 𝑥 ≤ 𝑋 ∧ 𝑥 ≤ ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) )
70 simplr ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
71 1 2 52 latlem12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ∈ 𝐵 ) ) → ( ( 𝑥 ≤ 𝑋 ∧ 𝑥 ≤ ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ↔ 𝑥 ≤ ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ) )
72 39 41 70 51 71 syl13anc ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ≤ 𝑋 ∧ 𝑥 ≤ ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ↔ 𝑥 ≤ ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ) )
73 69 72 mtbid ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 ≤ ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) )
74 73 nrexdv ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → ¬ ∃ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) )
75 simpll3 ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ≠ ( 0. ‘ 𝐾 ) ) → 𝐾 ∈ AtLat )
76 simpr ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
77 1 52 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ∈ 𝐵 ) → ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ∈ 𝐵 )
78 38 76 50 77 syl3anc ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ∈ 𝐵 )
79 78 adantr ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ≠ ( 0. ‘ 𝐾 ) ) → ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ∈ 𝐵 )
80 simpr ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ≠ ( 0. ‘ 𝐾 ) ) → ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ≠ ( 0. ‘ 𝐾 ) )
81 1 2 32 4 atlex ⊢ ( ( 𝐾 ∈ AtLat ∧ ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ∈ 𝐵 ∧ ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ≠ ( 0. ‘ 𝐾 ) ) → ∃ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) )
82 75 79 80 81 syl3anc ⊢ ( ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) ∧ ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ≠ ( 0. ‘ 𝐾 ) ) → ∃ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) )
83 82 ex ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ≠ ( 0. ‘ 𝐾 ) → ∃ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) ) )
84 83 necon1bd ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → ( ¬ ∃ 𝑥 ∈ 𝐴 𝑥 ≤ ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) → ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) = ( 0. ‘ 𝐾 ) ) )
85 74 84 mpd ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) = ( 0. ‘ 𝐾 ) )
86 1 2 52 48 32 omllaw3 ⊢ ( ( 𝐾 ∈ OML ∧ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ≤ 𝑋 ∧ ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) = ( 0. ‘ 𝐾 ) ) → ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) = 𝑋 ) )
87 45 43 76 86 syl3anc ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → ( ( ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ≤ 𝑋 ∧ ( 𝑋 ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) ) ) = ( 0. ‘ 𝐾 ) ) → ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) = 𝑋 ) )
88 19 85 87 mp2and ⊢ ( ( ( 𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat ) ∧ 𝑋 ∈ 𝐵 ) → ( 1 ‘ { 𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋 } ) = 𝑋 )