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