Proof of Theorem lhpbase
| Step | Hyp | Ref
| Expression |
| 1 | | n0i 4340 |
. . . 4
⊢ (𝑊 ∈ 𝐻 → ¬ 𝐻 = ∅) |
| 2 | | lhpbase.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
| 3 | 2 | eqeq1i 2742 |
. . . 4
⊢ (𝐻 = ∅ ↔
(LHyp‘𝐾) =
∅) |
| 4 | 1, 3 | sylnib 328 |
. . 3
⊢ (𝑊 ∈ 𝐻 → ¬ (LHyp‘𝐾) = ∅) |
| 5 | | fvprc 6898 |
. . 3
⊢ (¬
𝐾 ∈ V →
(LHyp‘𝐾) =
∅) |
| 6 | 4, 5 | nsyl2 141 |
. 2
⊢ (𝑊 ∈ 𝐻 → 𝐾 ∈ V) |
| 7 | | lhpbase.b |
. . . 4
⊢ 𝐵 = (Base‘𝐾) |
| 8 | | eqid 2737 |
. . . 4
⊢
(1.‘𝐾) =
(1.‘𝐾) |
| 9 | | eqid 2737 |
. . . 4
⊢ ( ⋖
‘𝐾) = ( ⋖
‘𝐾) |
| 10 | 7, 8, 9, 2 | islhp 39998 |
. . 3
⊢ (𝐾 ∈ V → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ 𝐵 ∧ 𝑊( ⋖ ‘𝐾)(1.‘𝐾)))) |
| 11 | 10 | simprbda 498 |
. 2
⊢ ((𝐾 ∈ V ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ 𝐵) |
| 12 | 6, 11 | mpancom 688 |
1
⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵) |