opnoncon - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > opnoncon		Structured version Visualization version GIF version

Theorem opnoncon 39707

Description: Law of contradiction for orthoposets. (chocin 31591 analog.) (Contributed by NM, 13-Sep-2011.)

**Hypotheses**
Ref	Expression
opnoncon.b	⊢ 𝐵 = (Base‘𝐾)
opnoncon.o	⊢ ⊥ = (oc‘𝐾)
opnoncon.m	⊢ ∧ = (meet‘𝐾)
opnoncon.z	⊢ 0 = (0.‘𝐾)

**Assertion**
Ref	Expression
opnoncon	⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 )

**Proof of Theorem opnoncon**
Step	Hyp	Ref	Expression
1		opnoncon.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
2		eqid 2740	. . . 4 ⊢ (le‘𝐾) = (le‘𝐾)
3		opnoncon.o	. . . 4 ⊢ ⊥ = (oc‘𝐾)
4		eqid 2740	. . . 4 ⊢ (join‘𝐾) = (join‘𝐾)
5		opnoncon.m	. . . 4 ⊢ ∧ = (meet‘𝐾)
6		opnoncon.z	. . . 4 ⊢ 0 = (0.‘𝐾)
7		eqid 2740	. . . 4 ⊢ (1.‘𝐾) = (1.‘𝐾)
8	1, 2, 3, 4, 5, 6, 7	oposlem 39681	. . 3 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 ))
9	8	3anidm23 1429	. 2 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 ))
10	9	simp3d 1150	1 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 )

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 class class class wbr 5079 ‘cfv 6492 (class class class)co 7363 Basecbs 17177 lecple 17225 occoc 17226 joincjn 18275 meetcmee 18276 0.cp0 18385 1.cp1 18386 OPcops 39671

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 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-ext 2712 ax-nul 5235

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-sb 2074 df-clab 2719 df-cleq 2732 df-clel 2815 df-ne 2936 df-ral 3055 df-rab 3393 df-v 3434 df-dif 3893 df-un 3895 df-ss 3907 df-nul 4269 df-if 4462 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4846 df-br 5080 df-dm 5635 df-iota 6448 df-fv 6500 df-ov 7366 df-oposet 39675

This theorem is referenced by: omlfh1N 39757 omlspjN 39760 atlatmstc 39818 pnonsingN 40432 lhpocnle 40515 dochnoncon 41890

W3C validator