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 39246

Description: Law of contradiction for orthoposets. (chocin 31470 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 2731	. . . 4 ⊢ (le‘𝐾) = (le‘𝐾)
3		opnoncon.o	. . . 4 ⊢ ⊥ = (oc‘𝐾)
4		eqid 2731	. . . 4 ⊢ (join‘𝐾) = (join‘𝐾)
5		opnoncon.m	. . . 4 ⊢ ∧ = (meet‘𝐾)
6		opnoncon.z	. . . 4 ⊢ 0 = (0.‘𝐾)
7		eqid 2731	. . . 4 ⊢ (1.‘𝐾) = (1.‘𝐾)
8	1, 2, 3, 4, 5, 6, 7	oposlem 39220	. . 3 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 ))
9	8	3anidm23 1423	. 2 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋(le‘𝐾)𝑋 → ( ⊥ ‘𝑋)(le‘𝐾)( ⊥ ‘𝑋))) ∧ (𝑋(join‘𝐾)( ⊥ ‘𝑋)) = (1.‘𝐾) ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 ))
10	9	simp3d 1144	1 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 )

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2111 class class class wbr 5091 ‘cfv 6481 (class class class)co 7346 Basecbs 17117 lecple 17165 occoc 17166 joincjn 18214 meetcmee 18215 0.cp0 18324 1.cp1 18325 OPcops 39210

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-ext 2703 ax-nul 5244

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-sb 2068 df-clab 2710 df-cleq 2723 df-clel 2806 df-ne 2929 df-ral 3048 df-rab 3396 df-v 3438 df-dif 3905 df-un 3907 df-ss 3919 df-nul 4284 df-if 4476 df-sn 4577 df-pr 4579 df-op 4583 df-uni 4860 df-br 5092 df-dm 5626 df-iota 6437 df-fv 6489 df-ov 7349 df-oposet 39214

This theorem is referenced by: omlfh1N 39296 omlspjN 39299 atlatmstc 39357 pnonsingN 39971 lhpocnle 40054 dochnoncon 41429

W3C validator