oposlem

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

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

Proof

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

Metamath Proof Explorer

Theorem oposlem

Proof