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 34924
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 29349 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 1085 . . . 4 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝐾 ∈ CLat)
2 ssrab2 3720 . . . . 5 {𝑦𝐵𝑦 𝑋} ⊆ 𝐵
3 atlatmstc.b . . . . . . 7 𝐵 = (Base‘𝐾)
4 atlatmstc.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
53, 4atssbase 34895 . . . . . 6 𝐴𝐵
6 rabss2 3718 . . . . . 6 (𝐴𝐵 → {𝑦𝐴𝑦 𝑋} ⊆ {𝑦𝐵𝑦 𝑋})
75, 6ax-mp 5 . . . . 5 {𝑦𝐴𝑦 𝑋} ⊆ {𝑦𝐵𝑦 𝑋}
8 atlatmstc.l . . . . . 6 = (le‘𝐾)
9 atlatmstc.u . . . . . 6 1 = (lub‘𝐾)
103, 8, 9lubss 17168 . . . . 5 ((𝐾 ∈ CLat ∧ {𝑦𝐵𝑦 𝑋} ⊆ 𝐵 ∧ {𝑦𝐴𝑦 𝑋} ⊆ {𝑦𝐵𝑦 𝑋}) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ( 1 ‘{𝑦𝐵𝑦 𝑋}))
112, 7, 10mp3an23 1456 . . . 4 (𝐾 ∈ CLat → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ( 1 ‘{𝑦𝐵𝑦 𝑋}))
121, 11syl 17 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ( 1 ‘{𝑦𝐵𝑦 𝑋}))
13 atlpos 34906 . . . . 5 (𝐾 ∈ AtLat → 𝐾 ∈ Poset)
14133ad2ant3 1104 . . . 4 ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) → 𝐾 ∈ Poset)
15 simpl 472 . . . . 5 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → 𝐾 ∈ Poset)
16 simpr 476 . . . . 5 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → 𝑋𝐵)
173, 8, 9, 15, 16lubid 17037 . . . 4 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐵𝑦 𝑋}) = 𝑋)
1814, 17sylan 487 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐵𝑦 𝑋}) = 𝑋)
1912, 18breqtrd 4711 . 2 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) 𝑋)
20 breq1 4688 . . . . . . . . . 10 (𝑦 = 𝑥 → (𝑦 𝑋𝑥 𝑋))
2120elrab 3396 . . . . . . . . 9 (𝑥 ∈ {𝑦𝐴𝑦 𝑋} ↔ (𝑥𝐴𝑥 𝑋))
22 simpll2 1121 . . . . . . . . . . 11 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥 ∈ {𝑦𝐴𝑦 𝑋}) → 𝐾 ∈ CLat)
23 ssrab2 3720 . . . . . . . . . . . . 13 {𝑦𝐴𝑦 𝑋} ⊆ 𝐴
2423, 5sstri 3645 . . . . . . . . . . . 12 {𝑦𝐴𝑦 𝑋} ⊆ 𝐵
253, 8, 9lubel 17169 . . . . . . . . . . . 12 ((𝐾 ∈ CLat ∧ 𝑥 ∈ {𝑦𝐴𝑦 𝑋} ∧ {𝑦𝐴𝑦 𝑋} ⊆ 𝐵) → 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}))
2624, 25mp3an3 1453 . . . . . . . . . . 11 ((𝐾 ∈ CLat ∧ 𝑥 ∈ {𝑦𝐴𝑦 𝑋}) → 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}))
2722, 26sylancom 702 . . . . . . . . . 10 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥 ∈ {𝑦𝐴𝑦 𝑋}) → 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}))
2827ex 449 . . . . . . . . 9 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → (𝑥 ∈ {𝑦𝐴𝑦 𝑋} → 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})))
2921, 28syl5bir 233 . . . . . . . 8 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ((𝑥𝐴𝑥 𝑋) → 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})))
3029expdimp 452 . . . . . . 7 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → (𝑥 𝑋𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})))
31 simpll3 1122 . . . . . . . . . . 11 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → 𝐾 ∈ AtLat)
32 eqid 2651 . . . . . . . . . . . 12 (0.‘𝐾) = (0.‘𝐾)
3332, 4atn0 34913 . . . . . . . . . . 11 ((𝐾 ∈ AtLat ∧ 𝑥𝐴) → 𝑥 ≠ (0.‘𝐾))
3431, 33sylancom 702 . . . . . . . . . 10 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → 𝑥 ≠ (0.‘𝐾))
3534adantr 480 . . . . . . . . 9 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) ∧ 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})) → 𝑥 ≠ (0.‘𝐾))
36 simpl3 1086 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝐾 ∈ AtLat)
37 atllat 34905 . . . . . . . . . . . . . . . 16 (𝐾 ∈ AtLat → 𝐾 ∈ Lat)
3836, 37syl 17 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝐾 ∈ Lat)
3938adantr 480 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → 𝐾 ∈ Lat)
403, 4atbase 34894 . . . . . . . . . . . . . . 15 (𝑥𝐴𝑥𝐵)
4140adantl 481 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → 𝑥𝐵)
423, 9clatlubcl 17159 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ CLat ∧ {𝑦𝐴𝑦 𝑋} ⊆ 𝐵) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵)
431, 24, 42sylancl 695 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵)
4443adantr 480 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵)
45 simpl1 1084 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝐾 ∈ OML)
46 omlop 34846 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ OML → 𝐾 ∈ OP)
4745, 46syl 17 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝐾 ∈ OP)
48 eqid 2651 . . . . . . . . . . . . . . . . 17 (oc‘𝐾) = (oc‘𝐾)
493, 48opoccl 34799 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ OP ∧ ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵) → ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) ∈ 𝐵)
5047, 43, 49syl2anc 694 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) ∈ 𝐵)
5150adantr 480 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) ∈ 𝐵)
52 eqid 2651 . . . . . . . . . . . . . . 15 (meet‘𝐾) = (meet‘𝐾)
533, 8, 52latlem12 17125 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ (𝑥𝐵 ∧ ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵 ∧ ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) ∈ 𝐵)) → ((𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∧ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))))
5439, 41, 44, 51, 53syl13anc 1368 . . . . . . . . . . . . 13 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ((𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∧ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))))
553, 48, 52, 32opnoncon 34813 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ OP ∧ ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵) → (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) = (0.‘𝐾))
5647, 43, 55syl2anc 694 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) = (0.‘𝐾))
5756breq2d 4697 . . . . . . . . . . . . . 14 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → (𝑥 (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 (0.‘𝐾)))
5857adantr 480 . . . . . . . . . . . . 13 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → (𝑥 (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 (0.‘𝐾)))
593, 8, 32ople0 34792 . . . . . . . . . . . . . 14 ((𝐾 ∈ OP ∧ 𝑥𝐵) → (𝑥 (0.‘𝐾) ↔ 𝑥 = (0.‘𝐾)))
6047, 40, 59syl2an 493 . . . . . . . . . . . . 13 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → (𝑥 (0.‘𝐾) ↔ 𝑥 = (0.‘𝐾)))
6154, 58, 603bitrd 294 . . . . . . . . . . . 12 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ((𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∧ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 = (0.‘𝐾)))
6261biimpa 500 . . . . . . . . . . 11 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) ∧ (𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∧ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))) → 𝑥 = (0.‘𝐾))
6362expr 642 . . . . . . . . . 10 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) ∧ 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})) → (𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) → 𝑥 = (0.‘𝐾)))
6463necon3ad 2836 . . . . . . . . 9 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) ∧ 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})) → (𝑥 ≠ (0.‘𝐾) → ¬ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
6535, 64mpd 15 . . . . . . . 8 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) ∧ 𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋})) → ¬ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))
6665ex 449 . . . . . . 7 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → (𝑥 ( 1 ‘{𝑦𝐴𝑦 𝑋}) → ¬ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
6730, 66syld 47 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → (𝑥 𝑋 → ¬ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
68 imnan 437 . . . . . 6 ((𝑥 𝑋 → ¬ 𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ ¬ (𝑥 𝑋𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
6967, 68sylib 208 . . . . 5 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ¬ (𝑥 𝑋𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
70 simplr 807 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → 𝑋𝐵)
713, 8, 52latlem12 17125 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑥𝐵𝑋𝐵 ∧ ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) ∈ 𝐵)) → ((𝑥 𝑋𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))))
7239, 41, 70, 51, 71syl13anc 1368 . . . . 5 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ((𝑥 𝑋𝑥 ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))))
7369, 72mtbid 313 . . . 4 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → ¬ 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
7473nrexdv 3030 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ¬ ∃𝑥𝐴 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
75 simpll3 1122 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾)) → 𝐾 ∈ AtLat)
76 simpr 476 . . . . . . . 8 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝑋𝐵)
773, 52latmcl 17099 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝑋𝐵 ∧ ((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})) ∈ 𝐵) → (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ∈ 𝐵)
7838, 76, 50, 77syl3anc 1366 . . . . . . 7 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ∈ 𝐵)
7978adantr 480 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾)) → (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ∈ 𝐵)
80 simpr 476 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾)) → (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾))
813, 8, 32, 4atlex 34921 . . . . . 6 ((𝐾 ∈ AtLat ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ∈ 𝐵 ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾)) → ∃𝑥𝐴 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
8275, 79, 80, 81syl3anc 1366 . . . . 5 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾)) → ∃𝑥𝐴 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))))
8382ex 449 . . . 4 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ((𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ≠ (0.‘𝐾) → ∃𝑥𝐴 𝑥 (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋})))))
8483necon1bd 2841 . . 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 34850 . . 3 ((𝐾 ∈ OML ∧ ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵𝑋𝐵) → ((( 1 ‘{𝑦𝐴𝑦 𝑋}) 𝑋 ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) = (0.‘𝐾)) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) = 𝑋))
8745, 43, 76, 86syl3anc 1366 . 2 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ((( 1 ‘{𝑦𝐴𝑦 𝑋}) 𝑋 ∧ (𝑋(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) = (0.‘𝐾)) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) = 𝑋))
8819, 85, 87mp2and 715 1 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) = 𝑋)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wrex 2942  {crab 2945  wss 3607   class class class wbr 4685  cfv 5926  (class class class)co 6690  Basecbs 15904  lecple 15995  occoc 15996  Posetcpo 16987  lubclub 16989  meetcmee 16992  0.cp0 17084  Latclat 17092  CLatccla 17154  OPcops 34777  OMLcoml 34780  Atomscatm 34868  AtLatcal 34869
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-preset 16975  df-poset 16993  df-plt 17005  df-lub 17021  df-glb 17022  df-join 17023  df-meet 17024  df-p0 17086  df-lat 17093  df-clat 17155  df-oposet 34781  df-ol 34783  df-oml 34784  df-covers 34871  df-ats 34872  df-atl 34903
This theorem is referenced by:  atlatle  34925  hlatmstcOLDN  35001  pmaple  35365  pol1N  35514  polpmapN  35516  pmaplubN  35528
  Copyright terms: Public domain W3C validator