This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ) )