Description: Projective subspace sum includes the set union of its arguments. (Contributed by NM, 12-Jan-2012) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | padd0.a | |- A = ( Atoms ` K ) |
|
padd0.p | |- .+ = ( +P ` K ) |
||
Assertion | paddunssN | |- ( ( K e. B /\ X C_ A /\ Y C_ A ) -> ( X u. Y ) C_ ( X .+ Y ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | padd0.a | |- A = ( Atoms ` K ) |
|
2 | padd0.p | |- .+ = ( +P ` K ) |
|
3 | ssun1 | |- ( X u. Y ) C_ ( ( X u. Y ) u. { p e. A | E. q e. X E. r e. Y p ( le ` K ) ( q ( join ` K ) r ) } ) |
|
4 | eqid | |- ( le ` K ) = ( le ` K ) |
|
5 | eqid | |- ( join ` K ) = ( join ` K ) |
|
6 | 4 5 1 2 | paddval | |- ( ( K e. B /\ X C_ A /\ Y C_ A ) -> ( X .+ Y ) = ( ( X u. Y ) u. { p e. A | E. q e. X E. r e. Y p ( le ` K ) ( q ( join ` K ) r ) } ) ) |
7 | 3 6 | sseqtrrid | |- ( ( K e. B /\ X C_ A /\ Y C_ A ) -> ( X u. Y ) C_ ( X .+ Y ) ) |