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 37781
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 31304 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 4037 . . . . 5 {𝑦𝐵𝑦 𝑋} ⊆ 𝐵
3 atlatmstc.b . . . . . . 7 𝐵 = (Base‘𝐾)
4 atlatmstc.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
53, 4atssbase 37752 . . . . . 6 𝐴𝐵
6 rabss2 4035 . . . . . 6 (𝐴𝐵 → {𝑦𝐴𝑦 𝑋} ⊆ {𝑦𝐵𝑦 𝑋})
75, 6ax-mp 5 . . . . 5 {𝑦𝐴𝑦 𝑋} ⊆ {𝑦𝐵𝑦 𝑋}
8 atlatmstc.l . . . . . 6 = (le‘𝐾)
9 atlatmstc.u . . . . . 6 1 = (lub‘𝐾)
103, 8, 9lubss 18402 . . . . 5 ((𝐾 ∈ CLat ∧ {𝑦𝐵𝑦 𝑋} ⊆ 𝐵 ∧ {𝑦𝐴𝑦 𝑋} ⊆ {𝑦𝐵𝑦 𝑋}) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ( 1 ‘{𝑦𝐵𝑦 𝑋}))
112, 7, 10mp3an23 1453 . . . 4 (𝐾 ∈ CLat → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ( 1 ‘{𝑦𝐵𝑦 𝑋}))
121, 11syl 17 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) ( 1 ‘{𝑦𝐵𝑦 𝑋}))
13 atlpos 37763 . . . . 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 18251 . . . 4 ((𝐾 ∈ Poset ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐵𝑦 𝑋}) = 𝑋)
1814, 17sylan 580 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐵𝑦 𝑋}) = 𝑋)
1912, 18breqtrd 5131 . 2 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → ( 1 ‘{𝑦𝐴𝑦 𝑋}) 𝑋)
20 breq1 5108 . . . . . . . . . 10 (𝑦 = 𝑥 → (𝑦 𝑋𝑥 𝑋))
2120elrab 3645 . . . . . . . . 9 (𝑥 ∈ {𝑦𝐴𝑦 𝑋} ↔ (𝑥𝐴𝑥 𝑋))
22 simpll2 1213 . . . . . . . . . . 11 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥 ∈ {𝑦𝐴𝑦 𝑋}) → 𝐾 ∈ CLat)
23 ssrab2 4037 . . . . . . . . . . . . 13 {𝑦𝐴𝑦 𝑋} ⊆ 𝐴
2423, 5sstri 3953 . . . . . . . . . . . 12 {𝑦𝐴𝑦 𝑋} ⊆ 𝐵
253, 8, 9lubel 18403 . . . . . . . . . . . 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 2736 . . . . . . . . . . . 12 (0.‘𝐾) = (0.‘𝐾)
3332, 4atn0 37770 . . . . . . . . . . 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 37762 . . . . . . . . . . . . . . . 16 (𝐾 ∈ AtLat → 𝐾 ∈ Lat)
3836, 37syl 17 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝐾 ∈ Lat)
3938adantr 481 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → 𝐾 ∈ Lat)
403, 4atbase 37751 . . . . . . . . . . . . . . 15 (𝑥𝐴𝑥𝐵)
4140adantl 482 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → 𝑥𝐵)
423, 9clatlubcl 18392 . . . . . . . . . . . . . . . 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 37703 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ OML → 𝐾 ∈ OP)
4745, 46syl 17 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → 𝐾 ∈ OP)
48 eqid 2736 . . . . . . . . . . . . . . . . 17 (oc‘𝐾) = (oc‘𝐾)
493, 48opoccl 37656 . . . . . . . . . . . . . . . 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 2736 . . . . . . . . . . . . . . 15 (meet‘𝐾) = (meet‘𝐾)
533, 8, 52latlem12 18355 . . . . . . . . . . . . . 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 37670 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ OP ∧ ( 1 ‘{𝑦𝐴𝑦 𝑋}) ∈ 𝐵) → (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) = (0.‘𝐾))
5647, 43, 55syl2anc 584 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) = (0.‘𝐾))
5756breq2d 5117 . . . . . . . . . . . . . 14 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) → (𝑥 (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 (0.‘𝐾)))
5857adantr 481 . . . . . . . . . . . . 13 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋𝐵) ∧ 𝑥𝐴) → (𝑥 (( 1 ‘{𝑦𝐴𝑦 𝑋})(meet‘𝐾)((oc‘𝐾)‘( 1 ‘{𝑦𝐴𝑦 𝑋}))) ↔ 𝑥 (0.‘𝐾)))
593, 8, 32ople0 37649 . . . . . . . . . . . . . 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 2956 . . . . . . . . 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 18355 . . . . . 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 3146 . . 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 18329 . . . . . . . 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 37778 . . . . . 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 2961 . . 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 37707 . . 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 2943  wrex 3073  {crab 3407  wss 3910   class class class wbr 5105  cfv 6496  (class class class)co 7357  Basecbs 17083  lecple 17140  occoc 17141  Posetcpo 18196  lubclub 18198  meetcmee 18201  0.cp0 18312  Latclat 18320  CLatccla 18387  OPcops 37634  OMLcoml 37637  Atomscatm 37725  AtLatcal 37726
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 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
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 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-proset 18184  df-poset 18202  df-plt 18219  df-lub 18235  df-glb 18236  df-join 18237  df-meet 18238  df-p0 18314  df-lat 18321  df-clat 18388  df-oposet 37638  df-ol 37640  df-oml 37641  df-covers 37728  df-ats 37729  df-atl 37760
This theorem is referenced by:  atlatle  37782  hlatmstcOLDN  37860  pmaple  38224  pol1N  38373  polpmapN  38375  pmaplubN  38387
  Copyright terms: Public domain W3C validator