Step |
Hyp |
Ref |
Expression |
1 |
|
llnbase.b |
|- B = ( Base ` K ) |
2 |
|
llnbase.n |
|- N = ( LLines ` K ) |
3 |
|
n0i |
|- ( X e. N -> -. N = (/) ) |
4 |
2
|
eqeq1i |
|- ( N = (/) <-> ( LLines ` K ) = (/) ) |
5 |
3 4
|
sylnib |
|- ( X e. N -> -. ( LLines ` K ) = (/) ) |
6 |
|
fvprc |
|- ( -. K e. _V -> ( LLines ` K ) = (/) ) |
7 |
5 6
|
nsyl2 |
|- ( X e. N -> K e. _V ) |
8 |
|
eqid |
|- ( |
9 |
|
eqid |
|- ( Atoms ` K ) = ( Atoms ` K ) |
10 |
1 8 9 2
|
islln |
|- ( K e. _V -> ( X e. N <-> ( X e. B /\ E. p e. ( Atoms ` K ) p ( |
11 |
10
|
simprbda |
|- ( ( K e. _V /\ X e. N ) -> X e. B ) |
12 |
7 11
|
mpancom |
|- ( X e. N -> X e. B ) |