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 37994
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 31478 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 4073 . . . . 5 {𝑦𝐵𝑦 𝑋} ⊆ 𝐵
3 atlatmstc.b . . . . . . 7 𝐵 = (Base‘𝐾)
4 atlatmstc.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
53, 4atssbase 37965 . . . . . 6 𝐴𝐵
6 rabss2 4071 . . . . . 6 (𝐴𝐵 → {𝑦𝐴𝑦 𝑋} ⊆ {𝑦𝐵𝑦 𝑋})
75, 6ax-mp 5 . . . . 5 {𝑦𝐴𝑦 𝑋} ⊆ {𝑦𝐵𝑦 𝑋}
8 atlatmstc.l . . . . . 6 = (le‘𝐾)
9 atlatmstc.u . . . . . 6 1 = (lub‘𝐾)
103, 8, 9lubss 18448 . . . . 5 ((𝐾 ∈ CLat ∧ {𝑦𝐵𝑦 𝑋} ⊆ 𝐵 ∧ {𝑦𝐴𝑦 𝑋} ⊆ {𝑦𝐵𝑦 𝑋}) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ( 1 ‘{𝑦𝐵𝑦 𝑋}))
112, 7, 10mp3an23 1453 . . . 4 (𝐾 ∈ CLat → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ( 1 ‘{𝑦𝐵𝑦 𝑋}))
121, 11syl 17 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ( 1 ‘{𝑦𝐵𝑦 𝑋}))
13 atlpos 37976 . . . . 5 (𝐾 ∈ AtLat → 𝐾 ∈ Poset)
14133ad2ant3 1135 . . . 4 ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) → 𝐾 ∈ Poset)
15 simpl 483 . . . . 5 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → 𝐾 ∈ Poset)
16 simpr 485 . . . . 5 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → 𝑋𝐵)
173, 8, 9, 15, 16lubid 18297 . . . 4 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐵𝑦 𝑋}) = 𝑋)
1814, 17sylan 580 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐵𝑦 𝑋}) = 𝑋)
1912, 18breqtrd 5167 . 2 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) 𝑋)
20 breq1 5144 . . . . . . . . . 10 (𝑦 = 𝑥 → (𝑦 𝑋𝑥 𝑋))
2120elrab 3679 . . . . . . . . 9 (𝑥 ∈ {𝑦𝐴𝑦 𝑋} ↔ (𝑥𝐴𝑥 𝑋))
22 simpll2 1213 . . . . . . . . . . 11 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥 ∈ {𝑦𝐴𝑦 𝑋}) → 𝐾 ∈ CLat)
23 ssrab2 4073 . . . . . . . . . . . . 13 {𝑦𝐴𝑦 𝑋} ⊆ 𝐴
2423, 5sstri 3987 . . . . . . . . . . . 12 {𝑦𝐴𝑦 𝑋} ⊆ 𝐵
253, 8, 9lubel 18449 . . . . . . . . . . . 12 ((𝐾 ∈ CLat ∧ 𝑥 ∈ {𝑦𝐴𝑦 𝑋} ∧ {𝑦𝐴𝑦 𝑋} ⊆ 𝐵) → 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}))
2624, 25mp3an3 1450 . . . . . . . . . . 11 ((𝐾 ∈ CLat ∧ 𝑥 ∈ {𝑦𝐴𝑦 𝑋}) → 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}))
2722, 26sylancom 588 . . . . . . . . . 10 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥 ∈ {𝑦𝐴𝑦 𝑋}) → 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}))
2827ex 413 . . . . . . . . 9 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → (𝑥 ∈ {𝑦𝐴𝑦 𝑋} → 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})))
2921, 28biimtrrid 242 . . . . . . . 8 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ((𝑥𝐴𝑥 𝑋) → 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})))
3029expdimp 453 . . . . . . 7 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → (𝑥 𝑋𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})))
31 simpll3 1214 . . . . . . . . . . 11 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → 𝐾 ∈ AtLat)
32 eqid 2731 . . . . . . . . . . . 12 (0.‘𝐾) = (0.‘𝐾)
3332, 4atn0 37983 . . . . . . . . . . 11 ((𝐾 ∈ AtLat ∧ 𝑥𝐴) → 𝑥 ≠ (0.‘𝐾))
3431, 33sylancom 588 . . . . . . . . . 10 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → 𝑥 ≠ (0.‘𝐾))
3534adantr 481 . . . . . . . . 9 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) ∧ 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})) → 𝑥 ≠ (0.‘𝐾))
36 simpl3 1193 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝐾 ∈ AtLat)
37 atllat 37975 . . . . . . . . . . . . . . . 16 (𝐾 ∈ AtLat → 𝐾 ∈ Lat)
3836, 37syl 17 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝐾 ∈ Lat)
3938adantr 481 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → 𝐾 ∈ Lat)
403, 4atbase 37964 . . . . . . . . . . . . . . 15 (𝑥𝐴𝑥𝐵)
4140adantl 482 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → 𝑥𝐵)
423, 9clatlubcl 18438 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ CLat ∧ {𝑦𝐴𝑦 𝑋} ⊆ 𝐵) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵)
431, 24, 42sylancl 586 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵)
4443adantr 481 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵)
45 simpl1 1191 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝐾 ∈ OML)
46 omlop 37916 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ OML → 𝐾 ∈ OP)
4745, 46syl 17 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝐾 ∈ OP)
48 eqid 2731 . . . . . . . . . . . . . . . . 17 (oc‘𝐾) = (oc‘𝐾)
493, 48opoccl 37869 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ OP ∧ ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵) → ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) ∈ 𝐵)
5047, 43, 49syl2anc 584 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) ∈ 𝐵)
5150adantr 481 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) ∈ 𝐵)
52 eqid 2731 . . . . . . . . . . . . . . 15 (meet‘𝐾) = (meet‘𝐾)
533, 8, 52latlem12 18401 . . . . . . . . . . . . . 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 37883 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ OP ∧ ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵) → (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) = (0.‘𝐾))
5647, 43, 55syl2anc 584 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) = (0.‘𝐾))
5756breq2d 5153 . . . . . . . . . . . . . 14 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → (𝑥 (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 (0.‘𝐾)))
5857adantr 481 . . . . . . . . . . . . 13 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → (𝑥 (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 (0.‘𝐾)))
593, 8, 32ople0 37862 . . . . . . . . . . . . . 14 ((𝐾 ∈ OP ∧ 𝑥𝐵) → (𝑥 (0.‘𝐾) ↔ 𝑥 = (0.‘𝐾)))
6047, 40, 59syl2an 596 . . . . . . . . . . . . 13 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → (𝑥 (0.‘𝐾) ↔ 𝑥 = (0.‘𝐾)))
6154, 58, 603bitrd 304 . . . . . . . . . . . 12 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ((𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∧ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 = (0.‘𝐾)))
6261biimpa 477 . . . . . . . . . . 11 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) ∧ (𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∧ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))) → 𝑥 = (0.‘𝐾))
6362expr 457 . . . . . . . . . 10 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) ∧ 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})) → (𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) → 𝑥 = (0.‘𝐾)))
6463necon3ad 2952 . . . . . . . . 9 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) ∧ 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})) → (𝑥 ≠ (0.‘𝐾) → ¬ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
6535, 64mpd 15 . . . . . . . 8 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) ∧ 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})) → ¬ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))
6665ex 413 . . . . . . 7 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → (𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}) → ¬ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
6730, 66syld 47 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → (𝑥 𝑋 → ¬ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
68 imnan 400 . . . . . 6 ((𝑥 𝑋 → ¬ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ ¬ (𝑥 𝑋𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
6967, 68sylib 217 . . . . 5 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ¬ (𝑥 𝑋𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
70 simplr 767 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → 𝑋𝐵)
713, 8, 52latlem12 18401 . . . . . 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 323 . . . 4 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ¬ 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
7473nrexdv 3148 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ¬ ∃𝑥𝐴 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
75 simpll3 1214 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾)) → 𝐾 ∈ AtLat)
76 simpr 485 . . . . . . . 8 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝑋𝐵)
773, 52latmcl 18375 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝑋𝐵 ∧ ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) ∈ 𝐵) → (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ∈ 𝐵)
7838, 76, 50, 77syl3anc 1371 . . . . . . 7 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ∈ 𝐵)
7978adantr 481 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾)) → (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ∈ 𝐵)
80 simpr 485 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾)) → (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾))
813, 8, 32, 4atlex 37991 . . . . . 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 413 . . . 4 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ((𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾) → ∃𝑥𝐴 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))))
8483necon1bd 2957 . . 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 37920 . . 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 697 1 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) = 𝑋)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wne 2939  wrex 3069  {crab 3431  wss 3944   class class class wbr 5141  cfv 6532  (class class class)co 7393  Basecbs 17126  lecple 17186  occoc 17187  Posetcpo 18242  lubclub 18244  meetcmee 18247  0.cp0 18358  Latclat 18366  CLatccla 18433  OPcops 37847  OMLcoml 37850  Atomscatm 37938  AtLatcal 37939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-riota 7349  df-ov 7396  df-oprab 7397  df-proset 18230  df-poset 18248  df-plt 18265  df-lub 18281  df-glb 18282  df-join 18283  df-meet 18284  df-p0 18360  df-lat 18367  df-clat 18434  df-oposet 37851  df-ol 37853  df-oml 37854  df-covers 37941  df-ats 37942  df-atl 37973
This theorem is referenced by:  atlatle  37995  hlatmstcOLDN  38073  pmaple  38437  pol1N  38586  polpmapN  38588  pmaplubN  38600
  Copyright terms: Public domain W3C validator