Step |
Hyp |
Ref |
Expression |
1 |
|
paddfval.l |
|- .<_ = ( le ` K ) |
2 |
|
paddfval.j |
|- .\/ = ( join ` K ) |
3 |
|
paddfval.a |
|- A = ( Atoms ` K ) |
4 |
|
paddfval.p |
|- .+ = ( +P ` K ) |
5 |
|
simpl1 |
|- ( ( ( K e. Lat /\ X C_ A /\ Q e. A ) /\ ( R e. X /\ S e. A /\ S .<_ ( R .\/ Q ) ) ) -> K e. Lat ) |
6 |
|
simpl2 |
|- ( ( ( K e. Lat /\ X C_ A /\ Q e. A ) /\ ( R e. X /\ S e. A /\ S .<_ ( R .\/ Q ) ) ) -> X C_ A ) |
7 |
|
simpl3 |
|- ( ( ( K e. Lat /\ X C_ A /\ Q e. A ) /\ ( R e. X /\ S e. A /\ S .<_ ( R .\/ Q ) ) ) -> Q e. A ) |
8 |
7
|
snssd |
|- ( ( ( K e. Lat /\ X C_ A /\ Q e. A ) /\ ( R e. X /\ S e. A /\ S .<_ ( R .\/ Q ) ) ) -> { Q } C_ A ) |
9 |
|
simpr1 |
|- ( ( ( K e. Lat /\ X C_ A /\ Q e. A ) /\ ( R e. X /\ S e. A /\ S .<_ ( R .\/ Q ) ) ) -> R e. X ) |
10 |
|
snidg |
|- ( Q e. A -> Q e. { Q } ) |
11 |
7 10
|
syl |
|- ( ( ( K e. Lat /\ X C_ A /\ Q e. A ) /\ ( R e. X /\ S e. A /\ S .<_ ( R .\/ Q ) ) ) -> Q e. { Q } ) |
12 |
|
simpr2 |
|- ( ( ( K e. Lat /\ X C_ A /\ Q e. A ) /\ ( R e. X /\ S e. A /\ S .<_ ( R .\/ Q ) ) ) -> S e. A ) |
13 |
|
simpr3 |
|- ( ( ( K e. Lat /\ X C_ A /\ Q e. A ) /\ ( R e. X /\ S e. A /\ S .<_ ( R .\/ Q ) ) ) -> S .<_ ( R .\/ Q ) ) |
14 |
1 2 3 4
|
elpaddri |
|- ( ( ( K e. Lat /\ X C_ A /\ { Q } C_ A ) /\ ( R e. X /\ Q e. { Q } ) /\ ( S e. A /\ S .<_ ( R .\/ Q ) ) ) -> S e. ( X .+ { Q } ) ) |
15 |
5 6 8 9 11 12 13 14
|
syl322anc |
|- ( ( ( K e. Lat /\ X C_ A /\ Q e. A ) /\ ( R e. X /\ S e. A /\ S .<_ ( R .\/ Q ) ) ) -> S e. ( X .+ { Q } ) ) |