Step |
Hyp |
Ref |
Expression |
1 |
|
llnbase.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
llnbase.n |
⊢ 𝑁 = ( LLines ‘ 𝐾 ) |
3 |
|
n0i |
⊢ ( 𝑋 ∈ 𝑁 → ¬ 𝑁 = ∅ ) |
4 |
2
|
eqeq1i |
⊢ ( 𝑁 = ∅ ↔ ( LLines ‘ 𝐾 ) = ∅ ) |
5 |
3 4
|
sylnib |
⊢ ( 𝑋 ∈ 𝑁 → ¬ ( LLines ‘ 𝐾 ) = ∅ ) |
6 |
|
fvprc |
⊢ ( ¬ 𝐾 ∈ V → ( LLines ‘ 𝐾 ) = ∅ ) |
7 |
5 6
|
nsyl2 |
⊢ ( 𝑋 ∈ 𝑁 → 𝐾 ∈ V ) |
8 |
|
eqid |
⊢ ( ⋖ ‘ 𝐾 ) = ( ⋖ ‘ 𝐾 ) |
9 |
|
eqid |
⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 ) |
10 |
1 8 9 2
|
islln |
⊢ ( 𝐾 ∈ V → ( 𝑋 ∈ 𝑁 ↔ ( 𝑋 ∈ 𝐵 ∧ ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) 𝑝 ( ⋖ ‘ 𝐾 ) 𝑋 ) ) ) |
11 |
10
|
simprbda |
⊢ ( ( 𝐾 ∈ V ∧ 𝑋 ∈ 𝑁 ) → 𝑋 ∈ 𝐵 ) |
12 |
7 11
|
mpancom |
⊢ ( 𝑋 ∈ 𝑁 → 𝑋 ∈ 𝐵 ) |