| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | oposlem.b | . . . . 5
⊢ 𝐵 = (Base‘𝐾) | 
| 2 |  | eqid 2737 | . . . . 5
⊢
(lub‘𝐾) =
(lub‘𝐾) | 
| 3 |  | eqid 2737 | . . . . 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 39181 | . . . 4
⊢ (𝐾 ∈ OP ↔ ((𝐾 ∈ Poset ∧ 𝐵 ∈ dom (lub‘𝐾) ∧ 𝐵 ∈ dom (glb‘𝐾)) ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((( ⊥ ‘𝑥) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥))) ∧ (𝑥 ∨ ( ⊥ ‘𝑥)) = 1 ∧ (𝑥 ∧ ( ⊥ ‘𝑥)) = 0 ))) | 
| 11 | 10 | simprbi 496 | . . 3
⊢ (𝐾 ∈ OP → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((( ⊥ ‘𝑥) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥))) ∧ (𝑥 ∨ ( ⊥ ‘𝑥)) = 1 ∧ (𝑥 ∧ ( ⊥ ‘𝑥)) = 0 )) | 
| 12 |  | fveq2 6906 | . . . . . . 7
⊢ (𝑥 = 𝑋 → ( ⊥ ‘𝑥) = ( ⊥ ‘𝑋)) | 
| 13 | 12 | eleq1d 2826 | . . . . . 6
⊢ (𝑥 = 𝑋 → (( ⊥ ‘𝑥) ∈ 𝐵 ↔ ( ⊥ ‘𝑋) ∈ 𝐵)) | 
| 14 |  | 2fveq3 6911 | . . . . . . 7
⊢ (𝑥 = 𝑋 → ( ⊥ ‘( ⊥
‘𝑥)) = ( ⊥
‘( ⊥ ‘𝑋))) | 
| 15 |  | id 22 | . . . . . . 7
⊢ (𝑥 = 𝑋 → 𝑥 = 𝑋) | 
| 16 | 14, 15 | eqeq12d 2753 | . . . . . 6
⊢ (𝑥 = 𝑋 → (( ⊥ ‘( ⊥
‘𝑥)) = 𝑥 ↔ ( ⊥ ‘( ⊥
‘𝑋)) = 𝑋)) | 
| 17 |  | breq1 5146 | . . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑥 ≤ 𝑦 ↔ 𝑋 ≤ 𝑦)) | 
| 18 | 12 | breq2d 5155 | . . . . . . 7
⊢ (𝑥 = 𝑋 → (( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥) ↔ ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑋))) | 
| 19 | 17, 18 | imbi12d 344 | . . . . . 6
⊢ (𝑥 = 𝑋 → ((𝑥 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥)) ↔ (𝑋 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑋)))) | 
| 20 | 13, 16, 19 | 3anbi123d 1438 | . . . . 5
⊢ (𝑥 = 𝑋 → ((( ⊥ ‘𝑥) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥))) ↔ (( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥
‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑋))))) | 
| 21 | 15, 12 | oveq12d 7449 | . . . . . 6
⊢ (𝑥 = 𝑋 → (𝑥 ∨ ( ⊥ ‘𝑥)) = (𝑋 ∨ ( ⊥ ‘𝑋))) | 
| 22 | 21 | eqeq1d 2739 | . . . . 5
⊢ (𝑥 = 𝑋 → ((𝑥 ∨ ( ⊥ ‘𝑥)) = 1 ↔ (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 )) | 
| 23 | 15, 12 | oveq12d 7449 | . . . . . 6
⊢ (𝑥 = 𝑋 → (𝑥 ∧ ( ⊥ ‘𝑥)) = (𝑋 ∧ ( ⊥ ‘𝑋))) | 
| 24 | 23 | eqeq1d 2739 | . . . . 5
⊢ (𝑥 = 𝑋 → ((𝑥 ∧ ( ⊥ ‘𝑥)) = 0 ↔ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 )) | 
| 25 | 20, 22, 24 | 3anbi123d 1438 | . . . 4
⊢ (𝑥 = 𝑋 → (((( ⊥ ‘𝑥) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥))) ∧ (𝑥 ∨ ( ⊥ ‘𝑥)) = 1 ∧ (𝑥 ∧ ( ⊥ ‘𝑥)) = 0 ) ↔ ((( ⊥
‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥
‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑋))) ∧ (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 ))) | 
| 26 |  | breq2 5147 | . . . . . . 7
⊢ (𝑦 = 𝑌 → (𝑋 ≤ 𝑦 ↔ 𝑋 ≤ 𝑌)) | 
| 27 |  | fveq2 6906 | . . . . . . . 8
⊢ (𝑦 = 𝑌 → ( ⊥ ‘𝑦) = ( ⊥ ‘𝑌)) | 
| 28 | 27 | breq1d 5153 | . . . . . . 7
⊢ (𝑦 = 𝑌 → (( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑋) ↔ ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) | 
| 29 | 26, 28 | imbi12d 344 | . . . . . 6
⊢ (𝑦 = 𝑌 → ((𝑋 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑋)) ↔ (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋)))) | 
| 30 | 29 | 3anbi3d 1444 | . . . . 5
⊢ (𝑦 = 𝑌 → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥
‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑋))) ↔ (( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥
‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))))) | 
| 31 | 30 | 3anbi1d 1442 | . . . 4
⊢ (𝑦 = 𝑌 → (((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥
‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑋))) ∧ (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 ) ↔ ((( ⊥
‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥
‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) ∧ (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 ))) | 
| 32 | 25, 31 | rspc2v 3633 | . . 3
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((( ⊥ ‘𝑥) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥 ∧ (𝑥 ≤ 𝑦 → ( ⊥ ‘𝑦) ≤ ( ⊥ ‘𝑥))) ∧ (𝑥 ∨ ( ⊥ ‘𝑥)) = 1 ∧ (𝑥 ∧ ( ⊥ ‘𝑥)) = 0 ) → ((( ⊥
‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥
‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) ∧ (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 ))) | 
| 33 | 11, 32 | mpan9 506 | . 2
⊢ ((𝐾 ∈ OP ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥
‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) ∧ (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 )) | 
| 34 | 33 | 3impb 1115 | 1
⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((( ⊥ ‘𝑋) ∈ 𝐵 ∧ ( ⊥ ‘( ⊥
‘𝑋)) = 𝑋 ∧ (𝑋 ≤ 𝑌 → ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) ∧ (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ∧ (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 )) |