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 39796

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1097 = wceq 1559 ∈ wcel 2141 class class class wbr 5099 ‘cfv 6517 (class class class)co 7392 Basecbs 17228 lecple 17276 occoc 17277 joincjn 18326 meetcmee 18327 0.cp0 18436 1.cp1 18437 OPcops 39760

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-ext 2733 ax-nul 5255

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-sb 2090 df-clab 2740 df-cleq 2753 df-clel 2836 df-ne 2957 df-ral 3076 df-rab 3414 df-v 3455 df-dif 3907 df-un 3909 df-ss 3921 df-nul 4286 df-if 4480 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-br 5100 df-dm 5655 df-iota 6473 df-fv 6525 df-ov 7395 df-oposet 39764

This theorem is referenced by: omlfh1N 39846 omlspjN 39849 atlatmstc 39907 pnonsingN 40521 lhpocnle 40604 dochnoncon 41979

W3C validator