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	$⊢ φ \to A \times A \subseteq V$
	ustund.2	$⊢ φ \to B \times B \subseteq V$
	ustund.3	$⊢ φ \to A \cap B \neq \emptyset$
Assertion	ustund	$⊢ φ \to (A \cup B) \times (A \cup B) \subseteq V \circ V$

Proof

Step	Hyp	Ref	Expression
1		ustund.1	$⊢ φ \to A \times A \subseteq V$
2		ustund.2	$⊢ φ \to B \times B \subseteq V$
3		ustund.3	$⊢ φ \to A \cap B \neq \emptyset$
4		xpco	$⊢ A \cap B \neq \emptyset \to ((A \cap B) \times (A \cup B)) \circ ((A \cup B) \times (A \cap B)) = (A \cup B) \times (A \cup B)$
5	3 4	syl	$⊢ φ \to ((A \cap B) \times (A \cup B)) \circ ((A \cup B) \times (A \cap B)) = (A \cup B) \times (A \cup B)$
6		xpundi	$⊢ (A \cap B) \times (A \cup B) = ((A \cap B) \times A) \cup ((A \cap B) \times B)$
7		xpindir	$⊢ (A \cap B) \times A = (A \times A) \cap (B \times A)$
8		inss1	$⊢ (A \times A) \cap (B \times A) \subseteq A \times A$
9	8 1	sstrid	$⊢ φ \to (A \times A) \cap (B \times A) \subseteq V$
10	7 9	eqsstrid	$⊢ φ \to (A \cap B) \times A \subseteq V$
11		xpindir	$⊢ (A \cap B) \times B = (A \times B) \cap (B \times B)$
12		inss2	$⊢ (A \times B) \cap (B \times B) \subseteq B \times B$
13	12 2	sstrid	$⊢ φ \to (A \times B) \cap (B \times B) \subseteq V$
14	11 13	eqsstrid	$⊢ φ \to (A \cap B) \times B \subseteq V$
15	10 14	unssd	$⊢ φ \to ((A \cap B) \times A) \cup ((A \cap B) \times B) \subseteq V$
16	6 15	eqsstrid	$⊢ φ \to (A \cap B) \times (A \cup B) \subseteq V$
17		xpundir	$⊢ (A \cup B) \times (A \cap B) = (A \times (A \cap B)) \cup (B \times (A \cap B))$
18		xpindi	$⊢ A \times (A \cap B) = (A \times A) \cap (A \times B)$
19		inss1	$⊢ (A \times A) \cap (A \times B) \subseteq A \times A$
20	19 1	sstrid	$⊢ φ \to (A \times A) \cap (A \times B) \subseteq V$
21	18 20	eqsstrid	$⊢ φ \to A \times (A \cap B) \subseteq V$
22		xpindi	$⊢ B \times (A \cap B) = (B \times A) \cap (B \times B)$
23		inss2	$⊢ (B \times A) \cap (B \times B) \subseteq B \times B$
24	23 2	sstrid	$⊢ φ \to (B \times A) \cap (B \times B) \subseteq V$
25	22 24	eqsstrid	$⊢ φ \to B \times (A \cap B) \subseteq V$
26	21 25	unssd	$⊢ φ \to (A \times (A \cap B)) \cup (B \times (A \cap B)) \subseteq V$
27	17 26	eqsstrid	$⊢ φ \to (A \cup B) \times (A \cap B) \subseteq V$
28	16 27	coss12d	$⊢ φ \to ((A \cap B) \times (A \cup B)) \circ ((A \cup B) \times (A \cap B)) \subseteq V \circ V$
29	5 28	eqsstrrd	$⊢ φ \to (A \cup B) \times (A \cup B) \subseteq V \circ V$

Metamath Proof Explorer

Theorem ustund

Proof