Theorem oposlem 40016

Description: Lemma for orthoposet properties. (Contributed by NM, 20-Oct-2011.)

Hypotheses

Ref	Expression
oposlem.b	⊢ 𝐵 = (Base‘𝐾)
oposlem.l	⊢ ≤ = (le‘𝐾)
oposlem.o	⊢ ⊥ = (oc‘𝐾)
oposlem.j	⊢ ∨ = (join‘𝐾)
oposlem.m	⊢ ∧ = (meet‘𝐾)
oposlem.f	⊢ 0 = (0.‘𝐾)
oposlem.u	⊢ 1 = (1.‘𝐾)

Assertion

Ref	Expression
oposlem	⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) ∧ (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 ))

Proof of Theorem oposlem

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oposlem.b	. . . . 5 ⊢ 𝐵 = (Base‘𝐾)
2		eqid 2765	. . . . 5 ⊢ (lub‘𝐾) = (lub‘𝐾)
3		eqid 2765	. . . . 5 ⊢ (glb‘𝐾) = (glb‘𝐾)
4		oposlem.l	. . . . 5 ⊢ ≤ = (le‘𝐾)
5		oposlem.o	. . . . 5 ⊢ ⊥ = (oc‘𝐾)
6		oposlem.j	. . . . 5 ⊢ ∨ = (join‘𝐾)
7		oposlem.m	. . . . 5 ⊢ ∧ = (meet‘𝐾)
8		oposlem.f	. . . . 5 ⊢ 0 = (0.‘𝐾)
9		oposlem.u	. . . . 5 ⊢ 1 = (1.‘𝐾)
10	1, 2, 3, 4, 5, 6, 7, 8, 9	isopos 40014	. . . 4 ⊢ (𝐾 ∈ OP ↔ ((𝐾 ∈ Poset ∧ 𝐵 ∈ dom (lub‘𝐾) ∧ 𝐵 ∈ dom (glb‘𝐾)) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((( ⊥ ‘𝑥) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥))) ∧ (𝑥 ∨ ( ⊥ ‘𝑥)) = 1 ∧ (𝑥 ∧ ( ⊥ ‘𝑥)) = 0 )))
11	10	simprbi 503	. . 3 ⊢ (𝐾 ∈ OP → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((( ⊥ ‘𝑥) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥))) ∧ (𝑥 ∨ ( ⊥ ‘𝑥)) = 1 ∧ (𝑥 ∧ ( ⊥ ‘𝑥)) = 0 ))
12		fveq2 6885	. . . . . . 7 ⊢ (𝑥 = 𝑋 → ( ⊥ ‘𝑥) = ( ⊥ ‘𝑋))
13	12	eleq1d 2850	. . . . . 6 ⊢ (𝑥 = 𝑋 → (( ⊥ ‘𝑥) ∈ 𝐵 ↔ ( ⊥ ‘𝑋) ∈ 𝐵))
14		2fveq3 6890	. . . . . . 7 ⊢ (𝑥 = 𝑋 → ( ⊥ ‘( ⊥ ‘𝑥)) = ( ⊥ ‘( ⊥ ‘𝑋)))
15		id 23	. . . . . . 7 ⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋)
16	14, 15	eqeq12d 2781	. . . . . 6 ⊢ (𝑥 = 𝑋 → (( ⊥ ‘( ⊥ ‘𝑥)) = 𝑥 ↔ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋))
17		breq1 5114	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (𝑥 ≤ 𝑦 ↔ 𝑋 ≤ 𝑦))
18	12	breq2d 5123	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥) ↔ ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑋)))
19	17, 18	imbi12d 347	. . . . . 6 ⊢ (𝑥 = 𝑋 → ((𝑥 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥)) ↔ (𝑋 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑋))))
20	13, 16, 19	3anbi123d 1464	. . . . 5 ⊢ (𝑥 = 𝑋 → ((( ⊥ ‘𝑥) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥))) ↔ (( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑋)))))
21	15, 12	oveq12d 7437	. . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑥 ∨ ( ⊥ ‘𝑥)) = (𝑋 ∨ ( ⊥ ‘𝑋)))
22	21	eqeq1d 2767	. . . . 5 ⊢ (𝑥 = 𝑋 → ((𝑥 ∨ ( ⊥ ‘𝑥)) = 1 ↔ (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ))
23	15, 12	oveq12d 7437	. . . . . 6 ⊢ (𝑥 = 𝑋 → (𝑥 ∧ ( ⊥ ‘𝑥)) = (𝑋 ∧ ( ⊥ ‘𝑋)))
24	23	eqeq1d 2767	. . . . 5 ⊢ (𝑥 = 𝑋 → ((𝑥 ∧ ( ⊥ ‘𝑥)) = 0 ↔ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 ))
25	20, 22, 24	3anbi123d 1464	. . . 4 ⊢ (𝑥 = 𝑋 → (((( ⊥ ‘𝑥) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥))) ∧ (𝑥 ∨ ( ⊥ ‘𝑥)) = 1 ∧ (𝑥 ∧ ( ⊥ ‘𝑥)) = 0 ) ↔ ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑋))) ∧ (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 )))
26		breq2 5115	. . . . . . 7 ⊢ (𝑦 = 𝑌 → (𝑋 ≤ 𝑦 ↔ 𝑋 ≤ 𝑌))
27		fveq2 6885	. . . . . . . 8 ⊢ (𝑦 = 𝑌 → ( ⊥ ‘𝑦) = ( ⊥ ‘𝑌))
28	27	breq1d 5121	. . . . . . 7 ⊢ (𝑦 = 𝑌 → (( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑋) ↔ ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋)))
29	26, 28	imbi12d 347	. . . . . 6 ⊢ (𝑦 = 𝑌 → ((𝑋 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑋)) ↔ (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))))
30	29	3anbi3d 1470	. . . . 5 ⊢ (𝑦 = 𝑌 → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑋))) ↔ (( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋)))))
31	30	3anbi1d 1468	. . . 4 ⊢ (𝑦 = 𝑌 → (((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑋))) ∧ (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 ) ↔ ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) ∧ (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 )))
32	25, 31	rspc2v 3594	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((( ⊥ ‘𝑥) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥))) ∧ (𝑥 ∨ ( ⊥ ‘𝑥)) = 1 ∧ (𝑥 ∧ ( ⊥ ‘𝑥)) = 0 ) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) ∧ (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 )))
33	11, 32	mpan9 516	. 2 ⊢ ((𝐾 ∈ OP ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) ∧ (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 ))
34	33	3impb 1132	1 ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) ∧ (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 ))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  ∀wral 3081   class class class wbr 5111  dom cdm 5663  ‘cfv 6540  (class class class)co 7419  Basecbs 17293  lecple 17341  occoc 17342  Posetcpo 18387  lubclub 18389  glbcglb 18390  joincjn 18391  meetcmee 18392  0.cp0 18501  1.cp1 18502  OPcops 40006

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-nul 5271

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-dm 5673  df-iota 6496  df-fv 6548  df-ov 7422  df-oposet 40010

This theorem is used by:  opoccl  40028  opococ  40029  oplecon3  40033  opexmid  40041  opnoncon  40042