Metamath Proof Explorer


Theorem paddunssN

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 ) )

Proof

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 ) )