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 40372

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 class class class wbr 5102 ‘cfv 6541 (class class class)co 7422 Basecbs 17394 lecple 17442 occoc 17443 joincjn 18492 meetcmee 18493 0.cp0 18602 1.cp1 18603 OPcops 40336

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-ext 2732 ax-nul 5259

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-sb 2099 df-clab 2739 df-cleq 2752 df-clel 2835 df-ne 2956 df-ral 3077 df-rab 3413 df-v 3452 df-ss 3897 df-dif 4046 df-un 4150 df-nul 4278 df-if 4482 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-br 5103 df-dm 5660 df-iota 6496 df-fv 6549 df-ov 7425 df-oposet 40340

This theorem is used by: omlfh1N 40422 omlspjN 40425 atlatmstc 40483 pnonsingN 41097 lhpocnle 41180 dochnoncon 42555

W3C validator