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 38275
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 31653 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 4077 . . . . 5 {𝑦 ∈ 𝐡 ∣ 𝑦 ≀ 𝑋} βŠ† 𝐡
3 atlatmstc.b . . . . . . 7 𝐡 = (Baseβ€˜πΎ)
4 atlatmstc.a . . . . . . 7 𝐴 = (Atomsβ€˜πΎ)
53, 4atssbase 38246 . . . . . 6 𝐴 βŠ† 𝐡
6 rabss2 4075 . . . . . 6 (𝐴 βŠ† 𝐡 β†’ {𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋} βŠ† {𝑦 ∈ 𝐡 ∣ 𝑦 ≀ 𝑋})
75, 6ax-mp 5 . . . . 5 {𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋} βŠ† {𝑦 ∈ 𝐡 ∣ 𝑦 ≀ 𝑋}
8 atlatmstc.l . . . . . 6 ≀ = (leβ€˜πΎ)
9 atlatmstc.u . . . . . 6 1 = (lubβ€˜πΎ)
103, 8, 9lubss 18468 . . . . 5 ((𝐾 ∈ CLat ∧ {𝑦 ∈ 𝐡 ∣ 𝑦 ≀ 𝑋} βŠ† 𝐡 ∧ {𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋} βŠ† {𝑦 ∈ 𝐡 ∣ 𝑦 ≀ 𝑋}) β†’ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) ≀ ( 1 β€˜{𝑦 ∈ 𝐡 ∣ 𝑦 ≀ 𝑋}))
112, 7, 10mp3an23 1453 . . . 4 (𝐾 ∈ CLat β†’ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) ≀ ( 1 β€˜{𝑦 ∈ 𝐡 ∣ 𝑦 ≀ 𝑋}))
121, 11syl 17 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) ≀ ( 1 β€˜{𝑦 ∈ 𝐡 ∣ 𝑦 ≀ 𝑋}))
13 atlpos 38257 . . . . 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 18317 . . . 4 ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐡) β†’ ( 1 β€˜{𝑦 ∈ 𝐡 ∣ 𝑦 ≀ 𝑋}) = 𝑋)
1814, 17sylan 580 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ ( 1 β€˜{𝑦 ∈ 𝐡 ∣ 𝑦 ≀ 𝑋}) = 𝑋)
1912, 18breqtrd 5174 . 2 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) ≀ 𝑋)
20 breq1 5151 . . . . . . . . . 10 (𝑦 = π‘₯ β†’ (𝑦 ≀ 𝑋 ↔ π‘₯ ≀ 𝑋))
2120elrab 3683 . . . . . . . . 9 (π‘₯ ∈ {𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋} ↔ (π‘₯ ∈ 𝐴 ∧ π‘₯ ≀ 𝑋))
22 simpll2 1213 . . . . . . . . . . 11 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ {𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) β†’ 𝐾 ∈ CLat)
23 ssrab2 4077 . . . . . . . . . . . . 13 {𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋} βŠ† 𝐴
2423, 5sstri 3991 . . . . . . . . . . . 12 {𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋} βŠ† 𝐡
253, 8, 9lubel 18469 . . . . . . . . . . . 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 2732 . . . . . . . . . . . 12 (0.β€˜πΎ) = (0.β€˜πΎ)
3332, 4atn0 38264 . . . . . . . . . . 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 38256 . . . . . . . . . . . . . . . 16 (𝐾 ∈ AtLat β†’ 𝐾 ∈ Lat)
3836, 37syl 17 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ 𝐾 ∈ Lat)
3938adantr 481 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) β†’ 𝐾 ∈ Lat)
403, 4atbase 38245 . . . . . . . . . . . . . . 15 (π‘₯ ∈ 𝐴 β†’ π‘₯ ∈ 𝐡)
4140adantl 482 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) β†’ π‘₯ ∈ 𝐡)
423, 9clatlubcl 18458 . . . . . . . . . . . . . . . 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 38197 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ OML β†’ 𝐾 ∈ OP)
4745, 46syl 17 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ 𝐾 ∈ OP)
48 eqid 2732 . . . . . . . . . . . . . . . . 17 (ocβ€˜πΎ) = (ocβ€˜πΎ)
493, 48opoccl 38150 . . . . . . . . . . . . . . . 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 2732 . . . . . . . . . . . . . . 15 (meetβ€˜πΎ) = (meetβ€˜πΎ)
533, 8, 52latlem12 18421 . . . . . . . . . . . . . 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 38164 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ OP ∧ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) ∈ 𝐡) β†’ (( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) = (0.β€˜πΎ))
5647, 43, 55syl2anc 584 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ (( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) = (0.β€˜πΎ))
5756breq2d 5160 . . . . . . . . . . . . . 14 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ (π‘₯ ≀ (( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) ↔ π‘₯ ≀ (0.β€˜πΎ)))
5857adantr 481 . . . . . . . . . . . . 13 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) β†’ (π‘₯ ≀ (( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) ↔ π‘₯ ≀ (0.β€˜πΎ)))
593, 8, 32ople0 38143 . . . . . . . . . . . . . 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 2953 . . . . . . . . 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 18421 . . . . . 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 3149 . . 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 18395 . . . . . . . 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 38272 . . . . . 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 2958 . . 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 38201 . . 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 2940  βˆƒwrex 3070  {crab 3432   βŠ† wss 3948   class class class wbr 5148  β€˜cfv 6543  (class class class)co 7411  Basecbs 17146  lecple 17206  occoc 17207  Posetcpo 18262  lubclub 18264  meetcmee 18267  0.cp0 18378  Latclat 18386  CLatccla 18453  OPcops 38128  OMLcoml 38131  Atomscatm 38219  AtLatcal 38220
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 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
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 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-proset 18250  df-poset 18268  df-plt 18285  df-lub 18301  df-glb 18302  df-join 18303  df-meet 18304  df-p0 18380  df-lat 18387  df-clat 18454  df-oposet 38132  df-ol 38134  df-oml 38135  df-covers 38222  df-ats 38223  df-atl 38254
This theorem is referenced by:  atlatle  38276  hlatmstcOLDN  38354  pmaple  38718  pol1N  38867  polpmapN  38869  pmaplubN  38881
  Copyright terms: Public domain W3C validator