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 |
1 2 3 4
|
elpadd2at |
|- ( ( K e. Lat /\ Q e. A /\ R e. A ) -> ( S e. ( { Q } .+ { R } ) <-> ( S e. A /\ S .<_ ( Q .\/ R ) ) ) ) |
6 |
5
|
3adant3r3 |
|- ( ( K e. Lat /\ ( Q e. A /\ R e. A /\ S e. A ) ) -> ( S e. ( { Q } .+ { R } ) <-> ( S e. A /\ S .<_ ( Q .\/ R ) ) ) ) |
7 |
|
simpr3 |
|- ( ( K e. Lat /\ ( Q e. A /\ R e. A /\ S e. A ) ) -> S e. A ) |
8 |
7
|
biantrurd |
|- ( ( K e. Lat /\ ( Q e. A /\ R e. A /\ S e. A ) ) -> ( S .<_ ( Q .\/ R ) <-> ( S e. A /\ S .<_ ( Q .\/ R ) ) ) ) |
9 |
6 8
|
bitr4d |
|- ( ( K e. Lat /\ ( Q e. A /\ R e. A /\ S e. A ) ) -> ( S e. ( { Q } .+ { R } ) <-> S .<_ ( Q .\/ R ) ) ) |