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 𝐴 = ( Atoms ‘ 𝐾 )
padd0.p + = ( +𝑃𝐾 )
Assertion paddunssN ( ( 𝐾𝐵𝑋𝐴𝑌𝐴 ) → ( 𝑋𝑌 ) ⊆ ( 𝑋 + 𝑌 ) )

Proof

Step Hyp Ref Expression
1 padd0.a 𝐴 = ( Atoms ‘ 𝐾 )
2 padd0.p + = ( +𝑃𝐾 )
3 ssun1 ( 𝑋𝑌 ) ⊆ ( ( 𝑋𝑌 ) ∪ { 𝑝𝐴 ∣ ∃ 𝑞𝑋𝑟𝑌 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) } )
4 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
5 eqid ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
6 4 5 1 2 paddval ( ( 𝐾𝐵𝑋𝐴𝑌𝐴 ) → ( 𝑋 + 𝑌 ) = ( ( 𝑋𝑌 ) ∪ { 𝑝𝐴 ∣ ∃ 𝑞𝑋𝑟𝑌 𝑝 ( le ‘ 𝐾 ) ( 𝑞 ( join ‘ 𝐾 ) 𝑟 ) } ) )
7 3 6 sseqtrrid ( ( 𝐾𝐵𝑋𝐴𝑌𝐴 ) → ( 𝑋𝑌 ) ⊆ ( 𝑋 + 𝑌 ) )