| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | lpolcon.o | . . 3
⊢ (𝜑 → ⊥ ∈ 𝑃) | 
| 2 |  | lpolcon.w | . . . 4
⊢ (𝜑 → 𝑊 ∈ 𝑋) | 
| 3 |  | lpolcon.v | . . . . 5
⊢ 𝑉 = (Base‘𝑊) | 
| 4 |  | eqid 2736 | . . . . 5
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) | 
| 5 |  | eqid 2736 | . . . . 5
⊢
(0g‘𝑊) = (0g‘𝑊) | 
| 6 |  | eqid 2736 | . . . . 5
⊢
(LSAtoms‘𝑊) =
(LSAtoms‘𝑊) | 
| 7 |  | eqid 2736 | . . . . 5
⊢
(LSHyp‘𝑊) =
(LSHyp‘𝑊) | 
| 8 |  | lpolcon.p | . . . . 5
⊢ 𝑃 = (LPol‘𝑊) | 
| 9 | 3, 4, 5, 6, 7, 8 | islpolN 41486 | . . . 4
⊢ (𝑊 ∈ 𝑋 → ( ⊥ ∈ 𝑃 ↔ ( ⊥ :𝒫 𝑉⟶(LSubSp‘𝑊) ∧ (( ⊥ ‘𝑉) = {(0g‘𝑊)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑊)(( ⊥ ‘𝑥) ∈ (LSHyp‘𝑊) ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥))))) | 
| 10 | 2, 9 | syl 17 | . . 3
⊢ (𝜑 → ( ⊥ ∈ 𝑃 ↔ ( ⊥ :𝒫 𝑉⟶(LSubSp‘𝑊) ∧ (( ⊥ ‘𝑉) = {(0g‘𝑊)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑊)(( ⊥ ‘𝑥) ∈ (LSHyp‘𝑊) ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥))))) | 
| 11 | 1, 10 | mpbid 232 | . 2
⊢ (𝜑 → ( ⊥ :𝒫 𝑉⟶(LSubSp‘𝑊) ∧ (( ⊥ ‘𝑉) = {(0g‘𝑊)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑊)(( ⊥ ‘𝑥) ∈ (LSHyp‘𝑊) ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥)))) | 
| 12 |  | simpr2 1195 | . . 3
⊢ (( ⊥
:𝒫 𝑉⟶(LSubSp‘𝑊) ∧ (( ⊥ ‘𝑉) = {(0g‘𝑊)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑊)(( ⊥ ‘𝑥) ∈ (LSHyp‘𝑊) ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥))) → ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥))) | 
| 13 |  | lpolcon.x | . . . . 5
⊢ (𝜑 → 𝑋 ⊆ 𝑉) | 
| 14 |  | lpolcon.y | . . . . 5
⊢ (𝜑 → 𝑌 ⊆ 𝑉) | 
| 15 |  | lpolcon.c | . . . . 5
⊢ (𝜑 → 𝑋 ⊆ 𝑌) | 
| 16 | 13, 14, 15 | 3jca 1128 | . . . 4
⊢ (𝜑 → (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑌)) | 
| 17 | 3 | fvexi 6919 | . . . . . . 7
⊢ 𝑉 ∈ V | 
| 18 | 17 | elpw2 5333 | . . . . . 6
⊢ (𝑋 ∈ 𝒫 𝑉 ↔ 𝑋 ⊆ 𝑉) | 
| 19 | 13, 18 | sylibr 234 | . . . . 5
⊢ (𝜑 → 𝑋 ∈ 𝒫 𝑉) | 
| 20 | 17 | elpw2 5333 | . . . . . 6
⊢ (𝑌 ∈ 𝒫 𝑉 ↔ 𝑌 ⊆ 𝑉) | 
| 21 | 14, 20 | sylibr 234 | . . . . 5
⊢ (𝜑 → 𝑌 ∈ 𝒫 𝑉) | 
| 22 |  | sseq1 4008 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝑥 ⊆ 𝑉 ↔ 𝑋 ⊆ 𝑉)) | 
| 23 |  | biidd 262 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝑦 ⊆ 𝑉 ↔ 𝑦 ⊆ 𝑉)) | 
| 24 |  | sseq1 4008 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝑥 ⊆ 𝑦 ↔ 𝑋 ⊆ 𝑦)) | 
| 25 | 22, 23, 24 | 3anbi123d 1437 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → ((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) ↔ (𝑋 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑦))) | 
| 26 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑥 = 𝑋 → ( ⊥ ‘𝑥) = ( ⊥ ‘𝑋)) | 
| 27 | 26 | sseq2d 4015 | . . . . . . . 8
⊢ (𝑥 = 𝑋 → (( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥) ↔ ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑋))) | 
| 28 | 25, 27 | imbi12d 344 | . . . . . . 7
⊢ (𝑥 = 𝑋 → (((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ↔ ((𝑋 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑋)))) | 
| 29 |  | biidd 262 | . . . . . . . . 9
⊢ (𝑦 = 𝑌 → (𝑋 ⊆ 𝑉 ↔ 𝑋 ⊆ 𝑉)) | 
| 30 |  | sseq1 4008 | . . . . . . . . 9
⊢ (𝑦 = 𝑌 → (𝑦 ⊆ 𝑉 ↔ 𝑌 ⊆ 𝑉)) | 
| 31 |  | sseq2 4009 | . . . . . . . . 9
⊢ (𝑦 = 𝑌 → (𝑋 ⊆ 𝑦 ↔ 𝑋 ⊆ 𝑌)) | 
| 32 | 29, 30, 31 | 3anbi123d 1437 | . . . . . . . 8
⊢ (𝑦 = 𝑌 → ((𝑋 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑦) ↔ (𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑌))) | 
| 33 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑦 = 𝑌 → ( ⊥ ‘𝑦) = ( ⊥ ‘𝑌)) | 
| 34 | 33 | sseq1d 4014 | . . . . . . . 8
⊢ (𝑦 = 𝑌 → (( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑋) ↔ ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋))) | 
| 35 | 32, 34 | imbi12d 344 | . . . . . . 7
⊢ (𝑦 = 𝑌 → (((𝑋 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑋)) ↔ ((𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑌) → ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋)))) | 
| 36 | 28, 35 | sylan9bb 509 | . . . . . 6
⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ↔ ((𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑌) → ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋)))) | 
| 37 | 36 | spc2gv 3599 | . . . . 5
⊢ ((𝑋 ∈ 𝒫 𝑉 ∧ 𝑌 ∈ 𝒫 𝑉) → (∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) → ((𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑌) → ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋)))) | 
| 38 | 19, 21, 37 | syl2anc 584 | . . . 4
⊢ (𝜑 → (∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) → ((𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ∧ 𝑋 ⊆ 𝑌) → ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋)))) | 
| 39 | 16, 38 | mpid 44 | . . 3
⊢ (𝜑 → (∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) → ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋))) | 
| 40 | 12, 39 | syl5 34 | . 2
⊢ (𝜑 → (( ⊥ :𝒫 𝑉⟶(LSubSp‘𝑊) ∧ (( ⊥ ‘𝑉) = {(0g‘𝑊)} ∧ ∀𝑥∀𝑦((𝑥 ⊆ 𝑉 ∧ 𝑦 ⊆ 𝑉 ∧ 𝑥 ⊆ 𝑦) → ( ⊥ ‘𝑦) ⊆ ( ⊥ ‘𝑥)) ∧ ∀𝑥 ∈ (LSAtoms‘𝑊)(( ⊥ ‘𝑥) ∈ (LSHyp‘𝑊) ∧ ( ⊥ ‘( ⊥
‘𝑥)) = 𝑥))) → ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋))) | 
| 41 | 11, 40 | mpd 15 | 1
⊢ (𝜑 → ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋)) |