Metamath Proof Explorer


Theorem shunssi

Description: Union is smaller than subspace sum. (Contributed by NM, 18-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses shincl.1 A S
shincl.2 B S
Assertion shunssi A B A + B

Proof

Step Hyp Ref Expression
1 shincl.1 A S
2 shincl.2 B S
3 1 sheli x A x
4 ax-hvaddid x x + 0 = x
5 4 eqcomd x x = x + 0
6 3 5 syl x A x = x + 0
7 sh0 B S 0 B
8 2 7 ax-mp 0 B
9 rspceov x A 0 B x = x + 0 y A z B x = y + z
10 8 9 mp3an2 x A x = x + 0 y A z B x = y + z
11 6 10 mpdan x A y A z B x = y + z
12 2 sheli x B x
13 hvaddid2 x 0 + x = x
14 13 eqcomd x x = 0 + x
15 12 14 syl x B x = 0 + x
16 sh0 A S 0 A
17 1 16 ax-mp 0 A
18 rspceov 0 A x B x = 0 + x y A z B x = y + z
19 17 18 mp3an1 x B x = 0 + x y A z B x = y + z
20 15 19 mpdan x B y A z B x = y + z
21 11 20 jaoi x A x B y A z B x = y + z
22 elun x A B x A x B
23 1 2 shseli x A + B y A z B x = y + z
24 21 22 23 3imtr4i x A B x A + B
25 24 ssriv A B A + B