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 38728
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 32159 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 1190 . . . 4 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ 𝐾 ∈ CLat)
2 ssrab2 4073 . . . . 5 {𝑦 ∈ 𝐡 ∣ 𝑦 ≀ 𝑋} βŠ† 𝐡
3 atlatmstc.b . . . . . . 7 𝐡 = (Baseβ€˜πΎ)
4 atlatmstc.a . . . . . . 7 𝐴 = (Atomsβ€˜πΎ)
53, 4atssbase 38699 . . . . . 6 𝐴 βŠ† 𝐡
6 rabss2 4071 . . . . . 6 (𝐴 βŠ† 𝐡 β†’ {𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋} βŠ† {𝑦 ∈ 𝐡 ∣ 𝑦 ≀ 𝑋})
75, 6ax-mp 5 . . . . 5 {𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋} βŠ† {𝑦 ∈ 𝐡 ∣ 𝑦 ≀ 𝑋}
8 atlatmstc.l . . . . . 6 ≀ = (leβ€˜πΎ)
9 atlatmstc.u . . . . . 6 1 = (lubβ€˜πΎ)
103, 8, 9lubss 18496 . . . . 5 ((𝐾 ∈ CLat ∧ {𝑦 ∈ 𝐡 ∣ 𝑦 ≀ 𝑋} βŠ† 𝐡 ∧ {𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋} βŠ† {𝑦 ∈ 𝐡 ∣ 𝑦 ≀ 𝑋}) β†’ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) ≀ ( 1 β€˜{𝑦 ∈ 𝐡 ∣ 𝑦 ≀ 𝑋}))
112, 7, 10mp3an23 1450 . . . 4 (𝐾 ∈ CLat β†’ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) ≀ ( 1 β€˜{𝑦 ∈ 𝐡 ∣ 𝑦 ≀ 𝑋}))
121, 11syl 17 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) ≀ ( 1 β€˜{𝑦 ∈ 𝐡 ∣ 𝑦 ≀ 𝑋}))
13 atlpos 38710 . . . . 5 (𝐾 ∈ AtLat β†’ 𝐾 ∈ Poset)
14133ad2ant3 1133 . . . 4 ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) β†’ 𝐾 ∈ Poset)
15 simpl 482 . . . . 5 ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐡) β†’ 𝐾 ∈ Poset)
16 simpr 484 . . . . 5 ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐡) β†’ 𝑋 ∈ 𝐡)
173, 8, 9, 15, 16lubid 18345 . . . 4 ((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐡) β†’ ( 1 β€˜{𝑦 ∈ 𝐡 ∣ 𝑦 ≀ 𝑋}) = 𝑋)
1814, 17sylan 579 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ ( 1 β€˜{𝑦 ∈ 𝐡 ∣ 𝑦 ≀ 𝑋}) = 𝑋)
1912, 18breqtrd 5168 . 2 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) ≀ 𝑋)
20 breq1 5145 . . . . . . . . . 10 (𝑦 = π‘₯ β†’ (𝑦 ≀ 𝑋 ↔ π‘₯ ≀ 𝑋))
2120elrab 3680 . . . . . . . . 9 (π‘₯ ∈ {𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋} ↔ (π‘₯ ∈ 𝐴 ∧ π‘₯ ≀ 𝑋))
22 simpll2 1211 . . . . . . . . . . 11 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ {𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) β†’ 𝐾 ∈ CLat)
23 ssrab2 4073 . . . . . . . . . . . . 13 {𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋} βŠ† 𝐴
2423, 5sstri 3987 . . . . . . . . . . . 12 {𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋} βŠ† 𝐡
253, 8, 9lubel 18497 . . . . . . . . . . . 12 ((𝐾 ∈ CLat ∧ π‘₯ ∈ {𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋} ∧ {𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋} βŠ† 𝐡) β†’ π‘₯ ≀ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))
2624, 25mp3an3 1447 . . . . . . . . . . 11 ((𝐾 ∈ CLat ∧ π‘₯ ∈ {𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) β†’ π‘₯ ≀ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))
2722, 26sylancom 587 . . . . . . . . . 10 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ {𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) β†’ π‘₯ ≀ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))
2827ex 412 . . . . . . . . 9 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ (π‘₯ ∈ {𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋} β†’ π‘₯ ≀ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})))
2921, 28biimtrrid 242 . . . . . . . 8 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ ((π‘₯ ∈ 𝐴 ∧ π‘₯ ≀ 𝑋) β†’ π‘₯ ≀ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})))
3029expdimp 452 . . . . . . 7 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) β†’ (π‘₯ ≀ 𝑋 β†’ π‘₯ ≀ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})))
31 simpll3 1212 . . . . . . . . . . 11 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) β†’ 𝐾 ∈ AtLat)
32 eqid 2727 . . . . . . . . . . . 12 (0.β€˜πΎ) = (0.β€˜πΎ)
3332, 4atn0 38717 . . . . . . . . . . 11 ((𝐾 ∈ AtLat ∧ π‘₯ ∈ 𝐴) β†’ π‘₯ β‰  (0.β€˜πΎ))
3431, 33sylancom 587 . . . . . . . . . 10 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) β†’ π‘₯ β‰  (0.β€˜πΎ))
3534adantr 480 . . . . . . . . 9 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) ∧ π‘₯ ≀ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})) β†’ π‘₯ β‰  (0.β€˜πΎ))
36 simpl3 1191 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ 𝐾 ∈ AtLat)
37 atllat 38709 . . . . . . . . . . . . . . . 16 (𝐾 ∈ AtLat β†’ 𝐾 ∈ Lat)
3836, 37syl 17 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ 𝐾 ∈ Lat)
3938adantr 480 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) β†’ 𝐾 ∈ Lat)
403, 4atbase 38698 . . . . . . . . . . . . . . 15 (π‘₯ ∈ 𝐴 β†’ π‘₯ ∈ 𝐡)
4140adantl 481 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) β†’ π‘₯ ∈ 𝐡)
423, 9clatlubcl 18486 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ CLat ∧ {𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋} βŠ† 𝐡) β†’ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) ∈ 𝐡)
431, 24, 42sylancl 585 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) ∈ 𝐡)
4443adantr 480 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) β†’ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) ∈ 𝐡)
45 simpl1 1189 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ 𝐾 ∈ OML)
46 omlop 38650 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ OML β†’ 𝐾 ∈ OP)
4745, 46syl 17 . . . . . . . . . . . . . . . 16 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ 𝐾 ∈ OP)
48 eqid 2727 . . . . . . . . . . . . . . . . 17 (ocβ€˜πΎ) = (ocβ€˜πΎ)
493, 48opoccl 38603 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ OP ∧ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) ∈ 𝐡) β†’ ((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})) ∈ 𝐡)
5047, 43, 49syl2anc 583 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ ((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})) ∈ 𝐡)
5150adantr 480 . . . . . . . . . . . . . 14 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) β†’ ((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})) ∈ 𝐡)
52 eqid 2727 . . . . . . . . . . . . . . 15 (meetβ€˜πΎ) = (meetβ€˜πΎ)
533, 8, 52latlem12 18449 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ (π‘₯ ∈ 𝐡 ∧ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) ∈ 𝐡 ∧ ((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})) ∈ 𝐡)) β†’ ((π‘₯ ≀ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) ∧ π‘₯ ≀ ((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) ↔ π‘₯ ≀ (( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})))))
5439, 41, 44, 51, 53syl13anc 1370 . . . . . . . . . . . . 13 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) β†’ ((π‘₯ ≀ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) ∧ π‘₯ ≀ ((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) ↔ π‘₯ ≀ (( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})))))
553, 48, 52, 32opnoncon 38617 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ OP ∧ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) ∈ 𝐡) β†’ (( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) = (0.β€˜πΎ))
5647, 43, 55syl2anc 583 . . . . . . . . . . . . . . 15 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ (( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) = (0.β€˜πΎ))
5756breq2d 5154 . . . . . . . . . . . . . 14 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ (π‘₯ ≀ (( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) ↔ π‘₯ ≀ (0.β€˜πΎ)))
5857adantr 480 . . . . . . . . . . . . 13 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) β†’ (π‘₯ ≀ (( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) ↔ π‘₯ ≀ (0.β€˜πΎ)))
593, 8, 32ople0 38596 . . . . . . . . . . . . . 14 ((𝐾 ∈ OP ∧ π‘₯ ∈ 𝐡) β†’ (π‘₯ ≀ (0.β€˜πΎ) ↔ π‘₯ = (0.β€˜πΎ)))
6047, 40, 59syl2an 595 . . . . . . . . . . . . 13 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) β†’ (π‘₯ ≀ (0.β€˜πΎ) ↔ π‘₯ = (0.β€˜πΎ)))
6154, 58, 603bitrd 305 . . . . . . . . . . . 12 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) β†’ ((π‘₯ ≀ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) ∧ π‘₯ ≀ ((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) ↔ π‘₯ = (0.β€˜πΎ)))
6261biimpa 476 . . . . . . . . . . 11 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) ∧ (π‘₯ ≀ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) ∧ π‘₯ ≀ ((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})))) β†’ π‘₯ = (0.β€˜πΎ))
6362expr 456 . . . . . . . . . 10 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) ∧ π‘₯ ≀ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})) β†’ (π‘₯ ≀ ((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})) β†’ π‘₯ = (0.β€˜πΎ)))
6463necon3ad 2948 . . . . . . . . 9 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) ∧ π‘₯ ≀ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})) β†’ (π‘₯ β‰  (0.β€˜πΎ) β†’ Β¬ π‘₯ ≀ ((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))))
6535, 64mpd 15 . . . . . . . 8 (((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) ∧ π‘₯ ≀ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})) β†’ Β¬ π‘₯ ≀ ((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})))
6665ex 412 . . . . . . 7 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) β†’ (π‘₯ ≀ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) β†’ Β¬ π‘₯ ≀ ((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))))
6730, 66syld 47 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) β†’ (π‘₯ ≀ 𝑋 β†’ Β¬ π‘₯ ≀ ((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))))
68 imnan 399 . . . . . 6 ((π‘₯ ≀ 𝑋 β†’ Β¬ π‘₯ ≀ ((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) ↔ Β¬ (π‘₯ ≀ 𝑋 ∧ π‘₯ ≀ ((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))))
6967, 68sylib 217 . . . . 5 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) β†’ Β¬ (π‘₯ ≀ 𝑋 ∧ π‘₯ ≀ ((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))))
70 simplr 768 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) β†’ 𝑋 ∈ 𝐡)
713, 8, 52latlem12 18449 . . . . . 6 ((𝐾 ∈ Lat ∧ (π‘₯ ∈ 𝐡 ∧ 𝑋 ∈ 𝐡 ∧ ((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})) ∈ 𝐡)) β†’ ((π‘₯ ≀ 𝑋 ∧ π‘₯ ≀ ((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) ↔ π‘₯ ≀ (𝑋(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})))))
7239, 41, 70, 51, 71syl13anc 1370 . . . . 5 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) β†’ ((π‘₯ ≀ 𝑋 ∧ π‘₯ ≀ ((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) ↔ π‘₯ ≀ (𝑋(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})))))
7369, 72mtbid 324 . . . 4 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ π‘₯ ∈ 𝐴) β†’ Β¬ π‘₯ ≀ (𝑋(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))))
7473nrexdv 3144 . . 3 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ Β¬ βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ (𝑋(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))))
75 simpll3 1212 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ (𝑋(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) β‰  (0.β€˜πΎ)) β†’ 𝐾 ∈ AtLat)
76 simpr 484 . . . . . . . 8 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ 𝑋 ∈ 𝐡)
773, 52latmcl 18423 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐡 ∧ ((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})) ∈ 𝐡) β†’ (𝑋(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) ∈ 𝐡)
7838, 76, 50, 77syl3anc 1369 . . . . . . 7 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ (𝑋(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) ∈ 𝐡)
7978adantr 480 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ (𝑋(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) β‰  (0.β€˜πΎ)) β†’ (𝑋(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) ∈ 𝐡)
80 simpr 484 . . . . . 6 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ (𝑋(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) β‰  (0.β€˜πΎ)) β†’ (𝑋(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) β‰  (0.β€˜πΎ))
813, 8, 32, 4atlex 38725 . . . . . 6 ((𝐾 ∈ AtLat ∧ (𝑋(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) ∈ 𝐡 ∧ (𝑋(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) β‰  (0.β€˜πΎ)) β†’ βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ (𝑋(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))))
8275, 79, 80, 81syl3anc 1369 . . . . 5 ((((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) ∧ (𝑋(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) β‰  (0.β€˜πΎ)) β†’ βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ (𝑋(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))))
8382ex 412 . . . 4 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ ((𝑋(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) β‰  (0.β€˜πΎ) β†’ βˆƒπ‘₯ ∈ 𝐴 π‘₯ ≀ (𝑋(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋})))))
8483necon1bd 2953 . . 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 38654 . . 3 ((𝐾 ∈ OML ∧ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) ∈ 𝐡 ∧ 𝑋 ∈ 𝐡) β†’ ((( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) ≀ 𝑋 ∧ (𝑋(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) = (0.β€˜πΎ)) β†’ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) = 𝑋))
8745, 43, 76, 86syl3anc 1369 . 2 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ ((( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) ≀ 𝑋 ∧ (𝑋(meetβ€˜πΎ)((ocβ€˜πΎ)β€˜( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}))) = (0.β€˜πΎ)) β†’ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) = 𝑋))
8819, 85, 87mp2and 698 1 (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐡) β†’ ( 1 β€˜{𝑦 ∈ 𝐴 ∣ 𝑦 ≀ 𝑋}) = 𝑋)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099   β‰  wne 2935  βˆƒwrex 3065  {crab 3427   βŠ† wss 3944   class class class wbr 5142  β€˜cfv 6542  (class class class)co 7414  Basecbs 17171  lecple 17231  occoc 17232  Posetcpo 18290  lubclub 18292  meetcmee 18295  0.cp0 18406  Latclat 18414  CLatccla 18481  OPcops 38581  OMLcoml 38584  Atomscatm 38672  AtLatcal 38673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7370  df-ov 7417  df-oprab 7418  df-proset 18278  df-poset 18296  df-plt 18313  df-lub 18329  df-glb 18330  df-join 18331  df-meet 18332  df-p0 18408  df-lat 18415  df-clat 18482  df-oposet 38585  df-ol 38587  df-oml 38588  df-covers 38675  df-ats 38676  df-atl 38707
This theorem is referenced by:  atlatle  38729  hlatmstcOLDN  38807  pmaple  39171  pol1N  39320  polpmapN  39322  pmaplubN  39334
  Copyright terms: Public domain W3C validator