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 36945
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 30289 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 1193 . . . 4 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝐾 ∈ CLat)
2 ssrab2 3967 . . . . 5 {𝑦𝐵𝑦 𝑋} ⊆ 𝐵
3 atlatmstc.b . . . . . . 7 𝐵 = (Base‘𝐾)
4 atlatmstc.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
53, 4atssbase 36916 . . . . . 6 𝐴𝐵
6 rabss2 3965 . . . . . 6 (𝐴𝐵 → {𝑦𝐴𝑦 𝑋} ⊆ {𝑦𝐵𝑦 𝑋})
75, 6ax-mp 5 . . . . 5 {𝑦𝐴𝑦 𝑋} ⊆ {𝑦𝐵𝑦 𝑋}
8 atlatmstc.l . . . . . 6 = (le‘𝐾)
9 atlatmstc.u . . . . . 6 1 = (lub‘𝐾)
103, 8, 9lubss 17840 . . . . 5 ((𝐾 ∈ CLat ∧ {𝑦𝐵𝑦 𝑋} ⊆ 𝐵 ∧ {𝑦𝐴𝑦 𝑋} ⊆ {𝑦𝐵𝑦 𝑋}) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ( 1 ‘{𝑦𝐵𝑦 𝑋}))
112, 7, 10mp3an23 1454 . . . 4 (𝐾 ∈ CLat → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ( 1 ‘{𝑦𝐵𝑦 𝑋}))
121, 11syl 17 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ( 1 ‘{𝑦𝐵𝑦 𝑋}))
13 atlpos 36927 . . . . 5 (𝐾 ∈ AtLat → 𝐾 ∈ Poset)
14133ad2ant3 1136 . . . 4 ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) → 𝐾 ∈ Poset)
15 simpl 486 . . . . 5 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → 𝐾 ∈ Poset)
16 simpr 488 . . . . 5 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → 𝑋𝐵)
173, 8, 9, 15, 16lubid 17709 . . . 4 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐵𝑦 𝑋}) = 𝑋)
1814, 17sylan 583 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐵𝑦 𝑋}) = 𝑋)
1912, 18breqtrd 5053 . 2 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) 𝑋)
20 breq1 5030 . . . . . . . . . 10 (𝑦 = 𝑥 → (𝑦 𝑋𝑥 𝑋))
2120elrab 3585 . . . . . . . . 9 (𝑥 ∈ {𝑦𝐴𝑦 𝑋} ↔ (𝑥𝐴𝑥 𝑋))
22 simpll2 1214 . . . . . . . . . . 11 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥 ∈ {𝑦𝐴𝑦 𝑋}) → 𝐾 ∈ CLat)
23 ssrab2 3967 . . . . . . . . . . . . 13 {𝑦𝐴𝑦 𝑋} ⊆ 𝐴
2423, 5sstri 3884 . . . . . . . . . . . 12 {𝑦𝐴𝑦 𝑋} ⊆ 𝐵
253, 8, 9lubel 17841 . . . . . . . . . . . 12 ((𝐾 ∈ CLat ∧ 𝑥 ∈ {𝑦𝐴𝑦 𝑋} ∧ {𝑦𝐴𝑦 𝑋} ⊆ 𝐵) → 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}))
2624, 25mp3an3 1451 . . . . . . . . . . 11 ((𝐾 ∈ CLat ∧ 𝑥 ∈ {𝑦𝐴𝑦 𝑋}) → 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}))
2722, 26sylancom 591 . . . . . . . . . 10 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥 ∈ {𝑦𝐴𝑦 𝑋}) → 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}))
2827ex 416 . . . . . . . . 9 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → (𝑥 ∈ {𝑦𝐴𝑦 𝑋} → 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})))
2921, 28syl5bir 246 . . . . . . . 8 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ((𝑥𝐴𝑥 𝑋) → 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})))
3029expdimp 456 . . . . . . 7 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → (𝑥 𝑋𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})))
31 simpll3 1215 . . . . . . . . . . 11 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → 𝐾 ∈ AtLat)
32 eqid 2738 . . . . . . . . . . . 12 (0.‘𝐾) = (0.‘𝐾)
3332, 4atn0 36934 . . . . . . . . . . 11 ((𝐾 ∈ AtLat ∧ 𝑥𝐴) → 𝑥 ≠ (0.‘𝐾))
3431, 33sylancom 591 . . . . . . . . . 10 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → 𝑥 ≠ (0.‘𝐾))
3534adantr 484 . . . . . . . . 9 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) ∧ 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})) → 𝑥 ≠ (0.‘𝐾))
36 simpl3 1194 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝐾 ∈ AtLat)
37 atllat 36926 . . . . . . . . . . . . . . . 16 (𝐾 ∈ AtLat → 𝐾 ∈ Lat)
3836, 37syl 17 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝐾 ∈ Lat)
3938adantr 484 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → 𝐾 ∈ Lat)
403, 4atbase 36915 . . . . . . . . . . . . . . 15 (𝑥𝐴𝑥𝐵)
4140adantl 485 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → 𝑥𝐵)
423, 9clatlubcl 17831 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ CLat ∧ {𝑦𝐴𝑦 𝑋} ⊆ 𝐵) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵)
431, 24, 42sylancl 589 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵)
4443adantr 484 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵)
45 simpl1 1192 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝐾 ∈ OML)
46 omlop 36867 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ OML → 𝐾 ∈ OP)
4745, 46syl 17 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝐾 ∈ OP)
48 eqid 2738 . . . . . . . . . . . . . . . . 17 (oc‘𝐾) = (oc‘𝐾)
493, 48opoccl 36820 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ OP ∧ ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵) → ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) ∈ 𝐵)
5047, 43, 49syl2anc 587 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) ∈ 𝐵)
5150adantr 484 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) ∈ 𝐵)
52 eqid 2738 . . . . . . . . . . . . . . 15 (meet‘𝐾) = (meet‘𝐾)
533, 8, 52latlem12 17797 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ (𝑥𝐵 ∧ ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵 ∧ ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) ∈ 𝐵)) → ((𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∧ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))))
5439, 41, 44, 51, 53syl13anc 1373 . . . . . . . . . . . . 13 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ((𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∧ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))))
553, 48, 52, 32opnoncon 36834 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ OP ∧ ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵) → (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) = (0.‘𝐾))
5647, 43, 55syl2anc 587 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) = (0.‘𝐾))
5756breq2d 5039 . . . . . . . . . . . . . 14 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → (𝑥 (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 (0.‘𝐾)))
5857adantr 484 . . . . . . . . . . . . 13 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → (𝑥 (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 (0.‘𝐾)))
593, 8, 32ople0 36813 . . . . . . . . . . . . . 14 ((𝐾 ∈ OP ∧ 𝑥𝐵) → (𝑥 (0.‘𝐾) ↔ 𝑥 = (0.‘𝐾)))
6047, 40, 59syl2an 599 . . . . . . . . . . . . 13 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → (𝑥 (0.‘𝐾) ↔ 𝑥 = (0.‘𝐾)))
6154, 58, 603bitrd 308 . . . . . . . . . . . 12 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ((𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∧ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 = (0.‘𝐾)))
6261biimpa 480 . . . . . . . . . . 11 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) ∧ (𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∧ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))) → 𝑥 = (0.‘𝐾))
6362expr 460 . . . . . . . . . 10 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) ∧ 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})) → (𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) → 𝑥 = (0.‘𝐾)))
6463necon3ad 2947 . . . . . . . . 9 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) ∧ 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})) → (𝑥 ≠ (0.‘𝐾) → ¬ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
6535, 64mpd 15 . . . . . . . 8 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) ∧ 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})) → ¬ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))
6665ex 416 . . . . . . 7 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → (𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}) → ¬ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
6730, 66syld 47 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → (𝑥 𝑋 → ¬ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
68 imnan 403 . . . . . 6 ((𝑥 𝑋 → ¬ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ ¬ (𝑥 𝑋𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
6967, 68sylib 221 . . . . 5 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ¬ (𝑥 𝑋𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
70 simplr 769 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → 𝑋𝐵)
713, 8, 52latlem12 17797 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑥𝐵𝑋𝐵 ∧ ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) ∈ 𝐵)) → ((𝑥 𝑋𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))))
7239, 41, 70, 51, 71syl13anc 1373 . . . . 5 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ((𝑥 𝑋𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))))
7369, 72mtbid 327 . . . 4 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ¬ 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
7473nrexdv 3179 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ¬ ∃𝑥𝐴 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
75 simpll3 1215 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾)) → 𝐾 ∈ AtLat)
76 simpr 488 . . . . . . . 8 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝑋𝐵)
773, 52latmcl 17771 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝑋𝐵 ∧ ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) ∈ 𝐵) → (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ∈ 𝐵)
7838, 76, 50, 77syl3anc 1372 . . . . . . 7 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ∈ 𝐵)
7978adantr 484 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾)) → (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ∈ 𝐵)
80 simpr 488 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾)) → (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾))
813, 8, 32, 4atlex 36942 . . . . . 6 ((𝐾 ∈ AtLat ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ∈ 𝐵 ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾)) → ∃𝑥𝐴 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
8275, 79, 80, 81syl3anc 1372 . . . . 5 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾)) → ∃𝑥𝐴 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
8382ex 416 . . . 4 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ((𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾) → ∃𝑥𝐴 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))))
8483necon1bd 2952 . . 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 36871 . . 3 ((𝐾 ∈ OML ∧ ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵𝑋𝐵) → ((( 1 ‘{𝑦𝐴𝑦 𝑋}) 𝑋 ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) = (0.‘𝐾)) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) = 𝑋))
8745, 43, 76, 86syl3anc 1372 . 2 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ((( 1 ‘{𝑦𝐴𝑦 𝑋}) 𝑋 ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) = (0.‘𝐾)) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) = 𝑋))
8819, 85, 87mp2and 699 1 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) = 𝑋)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1088   = wceq 1542  wcel 2113  wne 2934  wrex 3054  {crab 3057  wss 3841   class class class wbr 5027  cfv 6333  (class class class)co 7164  Basecbs 16579  lecple 16668  occoc 16669  Posetcpo 17659  lubclub 17661  meetcmee 17664  0.cp0 17756  Latclat 17764  CLatccla 17826  OPcops 36798  OMLcoml 36801  Atomscatm 36889  AtLatcal 36890
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5151  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-reu 3060  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-op 4520  df-uni 4794  df-iun 4880  df-br 5028  df-opab 5090  df-mpt 5108  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-riota 7121  df-ov 7167  df-oprab 7168  df-proset 17647  df-poset 17665  df-plt 17677  df-lub 17693  df-glb 17694  df-join 17695  df-meet 17696  df-p0 17758  df-lat 17765  df-clat 17827  df-oposet 36802  df-ol 36804  df-oml 36805  df-covers 36892  df-ats 36893  df-atl 36924
This theorem is referenced by:  atlatle  36946  hlatmstcOLDN  37023  pmaple  37387  pol1N  37536  polpmapN  37538  pmaplubN  37550
  Copyright terms: Public domain W3C validator