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 ⊢ ( 𝜑 → ( 𝐴 × 𝐴 ) ⊆ 𝑉 )
ustund.2 ⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) ⊆ 𝑉 )
ustund.3 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )
Assertion ustund ( 𝜑 → ( ( 𝐴 ∪ 𝐵 ) × ( 𝐴 ∪ 𝐵 ) ) ⊆ ( 𝑉 ∘ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 ustund.1 ⊢ ( 𝜑 → ( 𝐴 × 𝐴 ) ⊆ 𝑉 )
2 ustund.2 ⊢ ( 𝜑 → ( 𝐵 × 𝐵 ) ⊆ 𝑉 )
3 ustund.3 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )
4 xpco ⊢ ( ( 𝐴 ∩ 𝐵 ) ≠ ∅ → ( ( ( 𝐴 ∩ 𝐵 ) × ( 𝐴 ∪ 𝐵 ) ) ∘ ( ( 𝐴 ∪ 𝐵 ) × ( 𝐴 ∩ 𝐵 ) ) ) = ( ( 𝐴 ∪ 𝐵 ) × ( 𝐴 ∪ 𝐵 ) ) )
5 3 4 syl ⊢ ( 𝜑 → ( ( ( 𝐴 ∩ 𝐵 ) × ( 𝐴 ∪ 𝐵 ) ) ∘ ( ( 𝐴 ∪ 𝐵 ) × ( 𝐴 ∩ 𝐵 ) ) ) = ( ( 𝐴 ∪ 𝐵 ) × ( 𝐴 ∪ 𝐵 ) ) )
6 xpundi ⊢ ( ( 𝐴 ∩ 𝐵 ) × ( 𝐴 ∪ 𝐵 ) ) = ( ( ( 𝐴 ∩ 𝐵 ) × 𝐴 ) ∪ ( ( 𝐴 ∩ 𝐵 ) × 𝐵 ) )
7 xpindir ⊢ ( ( 𝐴 ∩ 𝐵 ) × 𝐴 ) = ( ( 𝐴 × 𝐴 ) ∩ ( 𝐵 × 𝐴 ) )
8 inss1 ⊢ ( ( 𝐴 × 𝐴 ) ∩ ( 𝐵 × 𝐴 ) ) ⊆ ( 𝐴 × 𝐴 )
9 8 1 sstrid ⊢ ( 𝜑 → ( ( 𝐴 × 𝐴 ) ∩ ( 𝐵 × 𝐴 ) ) ⊆ 𝑉 )
10 7 9 eqsstrid ⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝐵 ) × 𝐴 ) ⊆ 𝑉 )
11 xpindir ⊢ ( ( 𝐴 ∩ 𝐵 ) × 𝐵 ) = ( ( 𝐴 × 𝐵 ) ∩ ( 𝐵 × 𝐵 ) )
12 inss2 ⊢ ( ( 𝐴 × 𝐵 ) ∩ ( 𝐵 × 𝐵 ) ) ⊆ ( 𝐵 × 𝐵 )
13 12 2 sstrid ⊢ ( 𝜑 → ( ( 𝐴 × 𝐵 ) ∩ ( 𝐵 × 𝐵 ) ) ⊆ 𝑉 )
14 11 13 eqsstrid ⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝐵 ) × 𝐵 ) ⊆ 𝑉 )
15 10 14 unssd ⊢ ( 𝜑 → ( ( ( 𝐴 ∩ 𝐵 ) × 𝐴 ) ∪ ( ( 𝐴 ∩ 𝐵 ) × 𝐵 ) ) ⊆ 𝑉 )
16 6 15 eqsstrid ⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝐵 ) × ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑉 )
17 xpundir ⊢ ( ( 𝐴 ∪ 𝐵 ) × ( 𝐴 ∩ 𝐵 ) ) = ( ( 𝐴 × ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐵 × ( 𝐴 ∩ 𝐵 ) ) )
18 xpindi ⊢ ( 𝐴 × ( 𝐴 ∩ 𝐵 ) ) = ( ( 𝐴 × 𝐴 ) ∩ ( 𝐴 × 𝐵 ) )
19 inss1 ⊢ ( ( 𝐴 × 𝐴 ) ∩ ( 𝐴 × 𝐵 ) ) ⊆ ( 𝐴 × 𝐴 )
20 19 1 sstrid ⊢ ( 𝜑 → ( ( 𝐴 × 𝐴 ) ∩ ( 𝐴 × 𝐵 ) ) ⊆ 𝑉 )
21 18 20 eqsstrid ⊢ ( 𝜑 → ( 𝐴 × ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝑉 )
22 xpindi ⊢ ( 𝐵 × ( 𝐴 ∩ 𝐵 ) ) = ( ( 𝐵 × 𝐴 ) ∩ ( 𝐵 × 𝐵 ) )
23 inss2 ⊢ ( ( 𝐵 × 𝐴 ) ∩ ( 𝐵 × 𝐵 ) ) ⊆ ( 𝐵 × 𝐵 )
24 23 2 sstrid ⊢ ( 𝜑 → ( ( 𝐵 × 𝐴 ) ∩ ( 𝐵 × 𝐵 ) ) ⊆ 𝑉 )
25 22 24 eqsstrid ⊢ ( 𝜑 → ( 𝐵 × ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝑉 )
26 21 25 unssd ⊢ ( 𝜑 → ( ( 𝐴 × ( 𝐴 ∩ 𝐵 ) ) ∪ ( 𝐵 × ( 𝐴 ∩ 𝐵 ) ) ) ⊆ 𝑉 )
27 17 26 eqsstrid ⊢ ( 𝜑 → ( ( 𝐴 ∪ 𝐵 ) × ( 𝐴 ∩ 𝐵 ) ) ⊆ 𝑉 )
28 16 27 coss12d ⊢ ( 𝜑 → ( ( ( 𝐴 ∩ 𝐵 ) × ( 𝐴 ∪ 𝐵 ) ) ∘ ( ( 𝐴 ∪ 𝐵 ) × ( 𝐴 ∩ 𝐵 ) ) ) ⊆ ( 𝑉 ∘ 𝑉 ) )
29 5 28 eqsstrrd ⊢ ( 𝜑 → ( ( 𝐴 ∪ 𝐵 ) × ( 𝐴 ∪ 𝐵 ) ) ⊆ ( 𝑉 ∘ 𝑉 ) )