Proof of Theorem atbase
| Step | Hyp | Ref
| Expression |
| 1 | | n0i 4340 |
. . . 4
⊢ (𝑃 ∈ 𝐴 → ¬ 𝐴 = ∅) |
| 2 | | atombase.a |
. . . . 5
⊢ 𝐴 = (Atoms‘𝐾) |
| 3 | 2 | eqeq1i 2742 |
. . . 4
⊢ (𝐴 = ∅ ↔
(Atoms‘𝐾) =
∅) |
| 4 | 1, 3 | sylnib 328 |
. . 3
⊢ (𝑃 ∈ 𝐴 → ¬ (Atoms‘𝐾) = ∅) |
| 5 | | fvprc 6898 |
. . 3
⊢ (¬
𝐾 ∈ V →
(Atoms‘𝐾) =
∅) |
| 6 | 4, 5 | nsyl2 141 |
. 2
⊢ (𝑃 ∈ 𝐴 → 𝐾 ∈ V) |
| 7 | | atombase.b |
. . . 4
⊢ 𝐵 = (Base‘𝐾) |
| 8 | | eqid 2737 |
. . . 4
⊢
(0.‘𝐾) =
(0.‘𝐾) |
| 9 | | eqid 2737 |
. . . 4
⊢ ( ⋖
‘𝐾) = ( ⋖
‘𝐾) |
| 10 | 7, 8, 9, 2 | isat 39287 |
. . 3
⊢ (𝐾 ∈ V → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃))) |
| 11 | 10 | simprbda 498 |
. 2
⊢ ((𝐾 ∈ V ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐵) |
| 12 | 6, 11 | mpancom 688 |
1
⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵) |