Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  atlatmstc Structured version   Visualization version   GIF version

Theorem atlatmstc 39277
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 32396 analog.) (Contributed by NM, 5-Nov-2012.)
Hypotheses
Ref Expression
atlatmstc.b 𝐵 = (Base‘𝐾)
atlatmstc.l = (le‘𝐾)
atlatmstc.u 1 = (lub‘𝐾)
atlatmstc.a 𝐴 = (Atoms‘𝐾)
Assertion
Ref Expression
atlatmstc (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) = 𝑋)
Distinct variable groups:   𝑦,   𝑦,𝐴   𝑦,𝐵   𝑦,𝑋
Allowed substitution hints:   1 (𝑦)   𝐾(𝑦)

Proof of Theorem atlatmstc
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 simpl2 1192 . . . 4 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝐾 ∈ CLat)
2 ssrab2 4103 . . . . 5 {𝑦𝐵𝑦 𝑋} ⊆ 𝐵
3 atlatmstc.b . . . . . . 7 𝐵 = (Base‘𝐾)
4 atlatmstc.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
53, 4atssbase 39248 . . . . . 6 𝐴𝐵
6 rabss2 4101 . . . . . 6 (𝐴𝐵 → {𝑦𝐴𝑦 𝑋} ⊆ {𝑦𝐵𝑦 𝑋})
75, 6ax-mp 5 . . . . 5 {𝑦𝐴𝑦 𝑋} ⊆ {𝑦𝐵𝑦 𝑋}
8 atlatmstc.l . . . . . 6 = (le‘𝐾)
9 atlatmstc.u . . . . . 6 1 = (lub‘𝐾)
103, 8, 9lubss 18585 . . . . 5 ((𝐾 ∈ CLat ∧ {𝑦𝐵𝑦 𝑋} ⊆ 𝐵 ∧ {𝑦𝐴𝑦 𝑋} ⊆ {𝑦𝐵𝑦 𝑋}) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ( 1 ‘{𝑦𝐵𝑦 𝑋}))
112, 7, 10mp3an23 1453 . . . 4 (𝐾 ∈ CLat → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ( 1 ‘{𝑦𝐵𝑦 𝑋}))
121, 11syl 17 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ( 1 ‘{𝑦𝐵𝑦 𝑋}))
13 atlpos 39259 . . . . 5 (𝐾 ∈ AtLat → 𝐾 ∈ Poset)
14133ad2ant3 1135 . . . 4 ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) → 𝐾 ∈ Poset)
15 simpl 482 . . . . 5 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → 𝐾 ∈ Poset)
16 simpr 484 . . . . 5 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → 𝑋𝐵)
173, 8, 9, 15, 16lubid 18434 . . . 4 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐵𝑦 𝑋}) = 𝑋)
1814, 17sylan 579 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐵𝑦 𝑋}) = 𝑋)
1912, 18breqtrd 5192 . 2 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) 𝑋)
20 breq1 5169 . . . . . . . . . 10 (𝑦 = 𝑥 → (𝑦 𝑋𝑥 𝑋))
2120elrab 3708 . . . . . . . . 9 (𝑥 ∈ {𝑦𝐴𝑦 𝑋} ↔ (𝑥𝐴𝑥 𝑋))
22 simpll2 1213 . . . . . . . . . . 11 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥 ∈ {𝑦𝐴𝑦 𝑋}) → 𝐾 ∈ CLat)
23 ssrab2 4103 . . . . . . . . . . . . 13 {𝑦𝐴𝑦 𝑋} ⊆ 𝐴
2423, 5sstri 4018 . . . . . . . . . . . 12 {𝑦𝐴𝑦 𝑋} ⊆ 𝐵
253, 8, 9lubel 18586 . . . . . . . . . . . 12 ((𝐾 ∈ CLat ∧ 𝑥 ∈ {𝑦𝐴𝑦 𝑋} ∧ {𝑦𝐴𝑦 𝑋} ⊆ 𝐵) → 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}))
2624, 25mp3an3 1450 . . . . . . . . . . 11 ((𝐾 ∈ CLat ∧ 𝑥 ∈ {𝑦𝐴𝑦 𝑋}) → 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}))
2722, 26sylancom 587 . . . . . . . . . 10 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥 ∈ {𝑦𝐴𝑦 𝑋}) → 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}))
2827ex 412 . . . . . . . . 9 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → (𝑥 ∈ {𝑦𝐴𝑦 𝑋} → 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})))
2921, 28biimtrrid 243 . . . . . . . 8 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ((𝑥𝐴𝑥 𝑋) → 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})))
3029expdimp 452 . . . . . . 7 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → (𝑥 𝑋𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})))
31 simpll3 1214 . . . . . . . . . . 11 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → 𝐾 ∈ AtLat)
32 eqid 2740 . . . . . . . . . . . 12 (0.‘𝐾) = (0.‘𝐾)
3332, 4atn0 39266 . . . . . . . . . . 11 ((𝐾 ∈ AtLat ∧ 𝑥𝐴) → 𝑥 ≠ (0.‘𝐾))
3431, 33sylancom 587 . . . . . . . . . 10 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → 𝑥 ≠ (0.‘𝐾))
3534adantr 480 . . . . . . . . 9 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) ∧ 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})) → 𝑥 ≠ (0.‘𝐾))
36 simpl3 1193 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝐾 ∈ AtLat)
37 atllat 39258 . . . . . . . . . . . . . . . 16 (𝐾 ∈ AtLat → 𝐾 ∈ Lat)
3836, 37syl 17 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝐾 ∈ Lat)
3938adantr 480 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → 𝐾 ∈ Lat)
403, 4atbase 39247 . . . . . . . . . . . . . . 15 (𝑥𝐴𝑥𝐵)
4140adantl 481 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → 𝑥𝐵)
423, 9clatlubcl 18575 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ CLat ∧ {𝑦𝐴𝑦 𝑋} ⊆ 𝐵) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵)
431, 24, 42sylancl 585 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵)
4443adantr 480 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵)
45 simpl1 1191 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝐾 ∈ OML)
46 omlop 39199 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ OML → 𝐾 ∈ OP)
4745, 46syl 17 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝐾 ∈ OP)
48 eqid 2740 . . . . . . . . . . . . . . . . 17 (oc‘𝐾) = (oc‘𝐾)
493, 48opoccl 39152 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ OP ∧ ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵) → ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) ∈ 𝐵)
5047, 43, 49syl2anc 583 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) ∈ 𝐵)
5150adantr 480 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) ∈ 𝐵)
52 eqid 2740 . . . . . . . . . . . . . . 15 (meet‘𝐾) = (meet‘𝐾)
533, 8, 52latlem12 18538 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ (𝑥𝐵 ∧ ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵 ∧ ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) ∈ 𝐵)) → ((𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∧ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))))
5439, 41, 44, 51, 53syl13anc 1372 . . . . . . . . . . . . 13 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ((𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∧ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))))
553, 48, 52, 32opnoncon 39166 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ OP ∧ ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵) → (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) = (0.‘𝐾))
5647, 43, 55syl2anc 583 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) = (0.‘𝐾))
5756breq2d 5178 . . . . . . . . . . . . . 14 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → (𝑥 (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 (0.‘𝐾)))
5857adantr 480 . . . . . . . . . . . . 13 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → (𝑥 (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 (0.‘𝐾)))
593, 8, 32ople0 39145 . . . . . . . . . . . . . 14 ((𝐾 ∈ OP ∧ 𝑥𝐵) → (𝑥 (0.‘𝐾) ↔ 𝑥 = (0.‘𝐾)))
6047, 40, 59syl2an 595 . . . . . . . . . . . . 13 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → (𝑥 (0.‘𝐾) ↔ 𝑥 = (0.‘𝐾)))
6154, 58, 603bitrd 305 . . . . . . . . . . . 12 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ((𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∧ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 = (0.‘𝐾)))
6261biimpa 476 . . . . . . . . . . 11 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) ∧ (𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∧ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))) → 𝑥 = (0.‘𝐾))
6362expr 456 . . . . . . . . . 10 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) ∧ 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})) → (𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) → 𝑥 = (0.‘𝐾)))
6463necon3ad 2959 . . . . . . . . 9 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) ∧ 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})) → (𝑥 ≠ (0.‘𝐾) → ¬ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
6535, 64mpd 15 . . . . . . . 8 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) ∧ 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})) → ¬ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))
6665ex 412 . . . . . . 7 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → (𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}) → ¬ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
6730, 66syld 47 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → (𝑥 𝑋 → ¬ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
68 imnan 399 . . . . . 6 ((𝑥 𝑋 → ¬ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ ¬ (𝑥 𝑋𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
6967, 68sylib 218 . . . . 5 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ¬ (𝑥 𝑋𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
70 simplr 768 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → 𝑋𝐵)
713, 8, 52latlem12 18538 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑥𝐵𝑋𝐵 ∧ ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) ∈ 𝐵)) → ((𝑥 𝑋𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))))
7239, 41, 70, 51, 71syl13anc 1372 . . . . 5 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ((𝑥 𝑋𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))))
7369, 72mtbid 324 . . . 4 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ¬ 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
7473nrexdv 3155 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ¬ ∃𝑥𝐴 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
75 simpll3 1214 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾)) → 𝐾 ∈ AtLat)
76 simpr 484 . . . . . . . 8 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝑋𝐵)
773, 52latmcl 18512 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝑋𝐵 ∧ ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) ∈ 𝐵) → (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ∈ 𝐵)
7838, 76, 50, 77syl3anc 1371 . . . . . . 7 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ∈ 𝐵)
7978adantr 480 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾)) → (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ∈ 𝐵)
80 simpr 484 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾)) → (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾))
813, 8, 32, 4atlex 39274 . . . . . 6 ((𝐾 ∈ AtLat ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ∈ 𝐵 ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾)) → ∃𝑥𝐴 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
8275, 79, 80, 81syl3anc 1371 . . . . 5 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾)) → ∃𝑥𝐴 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
8382ex 412 . . . 4 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ((𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾) → ∃𝑥𝐴 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))))
8483necon1bd 2964 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → (¬ ∃𝑥𝐴 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) → (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) = (0.‘𝐾)))
8574, 84mpd 15 . 2 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) = (0.‘𝐾))
863, 8, 52, 48, 32omllaw3 39203 . . 3 ((𝐾 ∈ OML ∧ ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵𝑋𝐵) → ((( 1 ‘{𝑦𝐴𝑦 𝑋}) 𝑋 ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) = (0.‘𝐾)) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) = 𝑋))
8745, 43, 76, 86syl3anc 1371 . 2 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ((( 1 ‘{𝑦𝐴𝑦 𝑋}) 𝑋 ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) = (0.‘𝐾)) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) = 𝑋))
8819, 85, 87mp2and 698 1 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) = 𝑋)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1087   = wceq 1537  wcel 2108  wne 2946  wrex 3076  {crab 3443  wss 3976   class class class wbr 5166  cfv 6575  (class class class)co 7450  Basecbs 17260  lecple 17320  occoc 17321  Posetcpo 18379  lubclub 18381  meetcmee 18384  0.cp0 18495  Latclat 18503  CLatccla 18570  OPcops 39130  OMLcoml 39133  Atomscatm 39221  AtLatcal 39222
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7772
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6527  df-fun 6577  df-fn 6578  df-f 6579  df-f1 6580  df-fo 6581  df-f1o 6582  df-fv 6583  df-riota 7406  df-ov 7453  df-oprab 7454  df-proset 18367  df-poset 18385  df-plt 18402  df-lub 18418  df-glb 18419  df-join 18420  df-meet 18421  df-p0 18497  df-lat 18504  df-clat 18571  df-oposet 39134  df-ol 39136  df-oml 39137  df-covers 39224  df-ats 39225  df-atl 39256
This theorem is referenced by:  atlatle  39278  hlatmstcOLDN  39356  pmaple  39720  pol1N  39869  polpmapN  39871  pmaplubN  39883
  Copyright terms: Public domain W3C validator