Metamath Proof Explorer


Theorem ustund

Description: If two intersecting sets A and B are both small in V , their union is small in ( V ^ 2 ) . Proposition 1 of BourbakiTop1 p. II.12. This proposition actually does not require any axiom of the definition of uniform structures. (Contributed by Thierry Arnoux, 17-Nov-2017)

Ref Expression
Hypotheses ustund.1
|- ( ph -> ( A X. A ) C_ V )
ustund.2
|- ( ph -> ( B X. B ) C_ V )
ustund.3
|- ( ph -> ( A i^i B ) =/= (/) )
Assertion ustund
|- ( ph -> ( ( A u. B ) X. ( A u. B ) ) C_ ( V o. V ) )

Proof

Step Hyp Ref Expression
1 ustund.1
 |-  ( ph -> ( A X. A ) C_ V )
2 ustund.2
 |-  ( ph -> ( B X. B ) C_ V )
3 ustund.3
 |-  ( ph -> ( A i^i B ) =/= (/) )
4 xpco
 |-  ( ( A i^i B ) =/= (/) -> ( ( ( A i^i B ) X. ( A u. B ) ) o. ( ( A u. B ) X. ( A i^i B ) ) ) = ( ( A u. B ) X. ( A u. B ) ) )
5 3 4 syl
 |-  ( ph -> ( ( ( A i^i B ) X. ( A u. B ) ) o. ( ( A u. B ) X. ( A i^i B ) ) ) = ( ( A u. B ) X. ( A u. B ) ) )
6 xpundi
 |-  ( ( A i^i B ) X. ( A u. B ) ) = ( ( ( A i^i B ) X. A ) u. ( ( A i^i B ) X. B ) )
7 xpindir
 |-  ( ( A i^i B ) X. A ) = ( ( A X. A ) i^i ( B X. A ) )
8 inss1
 |-  ( ( A X. A ) i^i ( B X. A ) ) C_ ( A X. A )
9 8 1 sstrid
 |-  ( ph -> ( ( A X. A ) i^i ( B X. A ) ) C_ V )
10 7 9 eqsstrid
 |-  ( ph -> ( ( A i^i B ) X. A ) C_ V )
11 xpindir
 |-  ( ( A i^i B ) X. B ) = ( ( A X. B ) i^i ( B X. B ) )
12 inss2
 |-  ( ( A X. B ) i^i ( B X. B ) ) C_ ( B X. B )
13 12 2 sstrid
 |-  ( ph -> ( ( A X. B ) i^i ( B X. B ) ) C_ V )
14 11 13 eqsstrid
 |-  ( ph -> ( ( A i^i B ) X. B ) C_ V )
15 10 14 unssd
 |-  ( ph -> ( ( ( A i^i B ) X. A ) u. ( ( A i^i B ) X. B ) ) C_ V )
16 6 15 eqsstrid
 |-  ( ph -> ( ( A i^i B ) X. ( A u. B ) ) C_ V )
17 xpundir
 |-  ( ( A u. B ) X. ( A i^i B ) ) = ( ( A X. ( A i^i B ) ) u. ( B X. ( A i^i B ) ) )
18 xpindi
 |-  ( A X. ( A i^i B ) ) = ( ( A X. A ) i^i ( A X. B ) )
19 inss1
 |-  ( ( A X. A ) i^i ( A X. B ) ) C_ ( A X. A )
20 19 1 sstrid
 |-  ( ph -> ( ( A X. A ) i^i ( A X. B ) ) C_ V )
21 18 20 eqsstrid
 |-  ( ph -> ( A X. ( A i^i B ) ) C_ V )
22 xpindi
 |-  ( B X. ( A i^i B ) ) = ( ( B X. A ) i^i ( B X. B ) )
23 inss2
 |-  ( ( B X. A ) i^i ( B X. B ) ) C_ ( B X. B )
24 23 2 sstrid
 |-  ( ph -> ( ( B X. A ) i^i ( B X. B ) ) C_ V )
25 22 24 eqsstrid
 |-  ( ph -> ( B X. ( A i^i B ) ) C_ V )
26 21 25 unssd
 |-  ( ph -> ( ( A X. ( A i^i B ) ) u. ( B X. ( A i^i B ) ) ) C_ V )
27 17 26 eqsstrid
 |-  ( ph -> ( ( A u. B ) X. ( A i^i B ) ) C_ V )
28 16 27 coss12d
 |-  ( ph -> ( ( ( A i^i B ) X. ( A u. B ) ) o. ( ( A u. B ) X. ( A i^i B ) ) ) C_ ( V o. V ) )
29 5 28 eqsstrrd
 |-  ( ph -> ( ( A u. B ) X. ( A u. B ) ) C_ ( V o. V ) )