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	$$⊢\phi \to A\times A\subseteq V$$
	ustund.2	$$⊢\phi \to B\times B\subseteq V$$
	ustund.3	$$⊢\phi \to A\cap B\ne \varnothing$$
Assertion	ustund	$$⊢\phi \to \left(A\cup B\right)\times \left(A\cup B\right)\subseteq V\circ V$$

Proof

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