utop3cls

Description: Relation between a topological closure and a symmetric entourage in an uniform space. Second part of proposition 2 of BourbakiTop1 p. II.4. (Contributed by Thierry Arnoux, 17-Jan-2018)

		Ref	Expression
	Hypothesis	utoptop.1	$⊢ J = unifTop (U)$
	Assertion	utop3cls	$⊢ ((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \to cls (J \times_{t} J) (M) \subseteq V \circ (M \circ V)$

Proof

Step	Hyp	Ref	Expression
1		utoptop.1	$⊢ J = unifTop (U)$
2		relxp	$⊢ Rel (X \times X)$
3		utoptop	$⊢ U \in UnifOn (X) \to unifTop (U) \in Top$
4	1 3	eqeltrid	$⊢ U \in UnifOn (X) \to J \in Top$
5		txtop	$⊢ (J \in Top \land J \in Top) \to J \times_{t} J \in Top$
6	4 4 5	syl2anc	$⊢ U \in UnifOn (X) \to J \times_{t} J \in Top$
7	6	ad3antrrr	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to J \times_{t} J \in Top$
8		simpllr	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to M \subseteq X \times X$
9		utoptopon	$⊢ U \in UnifOn (X) \to unifTop (U) \in TopOn (X)$
10	1 9	eqeltrid	$⊢ U \in UnifOn (X) \to J \in TopOn (X)$
11		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
12	10 11	syl	$⊢ U \in UnifOn (X) \to X = ⋃ J$
13	12	sqxpeqd	$⊢ U \in UnifOn (X) \to X \times X = ⋃ J \times ⋃ J$
14		eqid	$⊢ ⋃ J = ⋃ J$
15	14 14	txuni	$⊢ (J \in Top \land J \in Top) \to ⋃ J \times ⋃ J = ⋃ (J \times_{t} J)$
16	4 4 15	syl2anc	$⊢ U \in UnifOn (X) \to ⋃ J \times ⋃ J = ⋃ (J \times_{t} J)$
17	13 16	eqtrd	$⊢ U \in UnifOn (X) \to X \times X = ⋃ (J \times_{t} J)$
18	17	ad3antrrr	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to X \times X = ⋃ (J \times_{t} J)$
19	8 18	sseqtrd	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to M \subseteq ⋃ (J \times_{t} J)$
20		eqid	$⊢ ⋃ (J \times_{t} J) = ⋃ (J \times_{t} J)$
21	20	clsss3	$⊢ (J \times_{t} J \in Top \land M \subseteq ⋃ (J \times_{t} J)) \to cls (J \times_{t} J) (M) \subseteq ⋃ (J \times_{t} J)$
22	7 19 21	syl2anc	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to cls (J \times_{t} J) (M) \subseteq ⋃ (J \times_{t} J)$
23	22 18	sseqtrrd	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to cls (J \times_{t} J) (M) \subseteq X \times X$
24		simpr	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to z \in cls (J \times_{t} J) (M)$
25	23 24	sseldd	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to z \in (X \times X)$
26		1st2nd	$⊢ (Rel (X \times X) \land z \in (X \times X)) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
27	2 25 26	sylancr	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
28		simp-4l	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to U \in UnifOn (X)$
29		simpr1l	$⊢ ((U \in UnifOn (X) \land M \subseteq X \times X) \land ((V \in U \land V^{-1} = V) \land z \in cls (J \times_{t} J) (M) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M))) \to V \in U$
30	29	3anassrs	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to V \in U$
31		ustrel	$⊢ (U \in UnifOn (X) \land V \in U) \to Rel V$
32	28 30 31	syl2anc	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to Rel V$
33		simpr	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)$
34		elin	$⊢ r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M) \leftrightarrow (r \in (V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \land r \in M)$
35	33 34	sylib	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to (r \in (V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \land r \in M)$
36	35	simpld	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to r \in (V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}])$
37		xp1st	$⊢ r \in (V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \to 1^{st} (r) \in V [\{1^{st} (z)\}]$
38	36 37	syl	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to 1^{st} (r) \in V [\{1^{st} (z)\}]$
39		elrelimasn	$⊢ Rel V \to (1^{st} (r) \in V [\{1^{st} (z)\}] \leftrightarrow 1^{st} (z) V 1^{st} (r))$
40	39	biimpa	$⊢ (Rel V \land 1^{st} (r) \in V [\{1^{st} (z)\}]) \to 1^{st} (z) V 1^{st} (r)$
41	32 38 40	syl2anc	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to 1^{st} (z) V 1^{st} (r)$
42		simp-4r	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to M \subseteq X \times X$
43		xpss	$⊢ X \times X \subseteq V \times V$
44	42 43	sstrdi	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to M \subseteq V \times V$
45		df-rel	$⊢ Rel M \leftrightarrow M \subseteq V \times V$
46	44 45	sylibr	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to Rel M$
47	35	simprd	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to r \in M$
48		1st2ndbr	$⊢ (Rel M \land r \in M) \to 1^{st} (r) M 2^{nd} (r)$
49	46 47 48	syl2anc	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to 1^{st} (r) M 2^{nd} (r)$
50		xp2nd	$⊢ r \in (V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \to 2^{nd} (r) \in V [\{2^{nd} (z)\}]$
51	36 50	syl	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to 2^{nd} (r) \in V [\{2^{nd} (z)\}]$
52		elrelimasn	$⊢ Rel V \to (2^{nd} (r) \in V [\{2^{nd} (z)\}] \leftrightarrow 2^{nd} (z) V 2^{nd} (r))$
53	52	biimpa	$⊢ (Rel V \land 2^{nd} (r) \in V [\{2^{nd} (z)\}]) \to 2^{nd} (z) V 2^{nd} (r)$
54	32 51 53	syl2anc	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to 2^{nd} (z) V 2^{nd} (r)$
55		simpr1r	$⊢ ((U \in UnifOn (X) \land M \subseteq X \times X) \land ((V \in U \land V^{-1} = V) \land z \in cls (J \times_{t} J) (M) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M))) \to V^{-1} = V$
56	55	3anassrs	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to V^{-1} = V$
57		breq	$⊢ V^{-1} = V \to (2^{nd} (r) V^{-1} 2^{nd} (z) \leftrightarrow 2^{nd} (r) V 2^{nd} (z))$
58		fvex	$⊢ 2^{nd} (r) \in V$
59		fvex	$⊢ 2^{nd} (z) \in V$
60	58 59	brcnv	$⊢ 2^{nd} (r) V^{-1} 2^{nd} (z) \leftrightarrow 2^{nd} (z) V 2^{nd} (r)$
61	57 60	bitr3di	$⊢ V^{-1} = V \to (2^{nd} (r) V 2^{nd} (z) \leftrightarrow 2^{nd} (z) V 2^{nd} (r))$
62	56 61	syl	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to (2^{nd} (r) V 2^{nd} (z) \leftrightarrow 2^{nd} (z) V 2^{nd} (r))$
63	54 62	mpbird	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to 2^{nd} (r) V 2^{nd} (z)$
64		fvex	$⊢ 1^{st} (z) \in V$
65		fvex	$⊢ 1^{st} (r) \in V$
66		brcogw	$⊢ ((1^{st} (z) \in V \land 2^{nd} (r) \in V \land 1^{st} (r) \in V) \land (1^{st} (z) V 1^{st} (r) \land 1^{st} (r) M 2^{nd} (r))) \to 1^{st} (z) (M \circ V) 2^{nd} (r)$
67	66	ex	$⊢ (1^{st} (z) \in V \land 2^{nd} (r) \in V \land 1^{st} (r) \in V) \to ((1^{st} (z) V 1^{st} (r) \land 1^{st} (r) M 2^{nd} (r)) \to 1^{st} (z) (M \circ V) 2^{nd} (r))$
68	64 58 65 67	mp3an	$⊢ (1^{st} (z) V 1^{st} (r) \land 1^{st} (r) M 2^{nd} (r)) \to 1^{st} (z) (M \circ V) 2^{nd} (r)$
69		brcogw	$⊢ ((1^{st} (z) \in V \land 2^{nd} (z) \in V \land 2^{nd} (r) \in V) \land (1^{st} (z) (M \circ V) 2^{nd} (r) \land 2^{nd} (r) V 2^{nd} (z))) \to 1^{st} (z) (V \circ (M \circ V)) 2^{nd} (z)$
70	69	ex	$⊢ (1^{st} (z) \in V \land 2^{nd} (z) \in V \land 2^{nd} (r) \in V) \to ((1^{st} (z) (M \circ V) 2^{nd} (r) \land 2^{nd} (r) V 2^{nd} (z)) \to 1^{st} (z) (V \circ (M \circ V)) 2^{nd} (z))$
71	64 59 58 70	mp3an	$⊢ (1^{st} (z) (M \circ V) 2^{nd} (r) \land 2^{nd} (r) V 2^{nd} (z)) \to 1^{st} (z) (V \circ (M \circ V)) 2^{nd} (z)$
72	68 71	sylan	$⊢ ((1^{st} (z) V 1^{st} (r) \land 1^{st} (r) M 2^{nd} (r)) \land 2^{nd} (r) V 2^{nd} (z)) \to 1^{st} (z) (V \circ (M \circ V)) 2^{nd} (z)$
73	41 49 63 72	syl21anc	$⊢ ((((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \land r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M)) \to 1^{st} (z) (V \circ (M \circ V)) 2^{nd} (z)$
74	73	ralrimiva	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to \forall r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M) 1^{st} (z) (V \circ (M \circ V)) 2^{nd} (z)$
75		simplll	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to U \in UnifOn (X)$
76		simplrl	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to V \in U$
77	4	3ad2ant1	$⊢ (U \in UnifOn (X) \land V \in U \land z \in (X \times X)) \to J \in Top$
78		xp1st	$⊢ z \in (X \times X) \to 1^{st} (z) \in X$
79	1	utopsnnei	$⊢ (U \in UnifOn (X) \land V \in U \land 1^{st} (z) \in X) \to V [\{1^{st} (z)\}] \in nei (J) (\{1^{st} (z)\})$
80	78 79	syl3an3	$⊢ (U \in UnifOn (X) \land V \in U \land z \in (X \times X)) \to V [\{1^{st} (z)\}] \in nei (J) (\{1^{st} (z)\})$
81		xp2nd	$⊢ z \in (X \times X) \to 2^{nd} (z) \in X$
82	1	utopsnnei	$⊢ (U \in UnifOn (X) \land V \in U \land 2^{nd} (z) \in X) \to V [\{2^{nd} (z)\}] \in nei (J) (\{2^{nd} (z)\})$
83	81 82	syl3an3	$⊢ (U \in UnifOn (X) \land V \in U \land z \in (X \times X)) \to V [\{2^{nd} (z)\}] \in nei (J) (\{2^{nd} (z)\})$
84	14 14	neitx	$⊢ ((J \in Top \land J \in Top) \land (V [\{1^{st} (z)\}] \in nei (J) (\{1^{st} (z)\}) \land V [\{2^{nd} (z)\}] \in nei (J) (\{2^{nd} (z)\}))) \to V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}] \in nei (J \times_{t} J) (\{1^{st} (z)\} \times \{2^{nd} (z)\})$
85	77 77 80 83 84	syl22anc	$⊢ (U \in UnifOn (X) \land V \in U \land z \in (X \times X)) \to V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}] \in nei (J \times_{t} J) (\{1^{st} (z)\} \times \{2^{nd} (z)\})$
86		1st2nd2	$⊢ z \in (X \times X) \to z = ⟨1^{st} (z), 2^{nd} (z)⟩$
87	86	sneqd	$⊢ z \in (X \times X) \to \{z\} = \{⟨1^{st} (z), 2^{nd} (z)⟩\}$
88	64 59	xpsn	$⊢ \{1^{st} (z)\} \times \{2^{nd} (z)\} = \{⟨1^{st} (z), 2^{nd} (z)⟩\}$
89	87 88	eqtr4di	$⊢ z \in (X \times X) \to \{z\} = \{1^{st} (z)\} \times \{2^{nd} (z)\}$
90	89	fveq2d	$⊢ z \in (X \times X) \to nei (J \times_{t} J) (\{z\}) = nei (J \times_{t} J) (\{1^{st} (z)\} \times \{2^{nd} (z)\})$
91	90	3ad2ant3	$⊢ (U \in UnifOn (X) \land V \in U \land z \in (X \times X)) \to nei (J \times_{t} J) (\{z\}) = nei (J \times_{t} J) (\{1^{st} (z)\} \times \{2^{nd} (z)\})$
92	85 91	eleqtrrd	$⊢ (U \in UnifOn (X) \land V \in U \land z \in (X \times X)) \to V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}] \in nei (J \times_{t} J) (\{z\})$
93	75 76 25 92	syl3anc	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}] \in nei (J \times_{t} J) (\{z\})$
94	20	neindisj	$⊢ ((J \times_{t} J \in Top \land M \subseteq ⋃ (J \times_{t} J)) \land (z \in cls (J \times_{t} J) (M) \land V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}] \in nei (J \times_{t} J) (\{z\}))) \to (V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M \neq \emptyset$
95	7 19 24 93 94	syl22anc	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to (V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M \neq \emptyset$
96		r19.3rzv	$⊢ (V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M \neq \emptyset \to (1^{st} (z) (V \circ (M \circ V)) 2^{nd} (z) \leftrightarrow \forall r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M) 1^{st} (z) (V \circ (M \circ V)) 2^{nd} (z))$
97	95 96	syl	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to (1^{st} (z) (V \circ (M \circ V)) 2^{nd} (z) \leftrightarrow \forall r \in ((V [\{1^{st} (z)\}] \times V [\{2^{nd} (z)\}]) \cap M) 1^{st} (z) (V \circ (M \circ V)) 2^{nd} (z))$
98	74 97	mpbird	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to 1^{st} (z) (V \circ (M \circ V)) 2^{nd} (z)$
99		df-br	$⊢ 1^{st} (z) (V \circ (M \circ V)) 2^{nd} (z) \leftrightarrow ⟨1^{st} (z), 2^{nd} (z)⟩ \in (V \circ (M \circ V))$
100	98 99	sylib	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to ⟨1^{st} (z), 2^{nd} (z)⟩ \in (V \circ (M \circ V))$
101	27 100	eqeltrd	$⊢ (((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \land z \in cls (J \times_{t} J) (M)) \to z \in (V \circ (M \circ V))$
102	101	ex	$⊢ ((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \to (z \in cls (J \times_{t} J) (M) \to z \in (V \circ (M \circ V)))$
103	102	ssrdv	$⊢ ((U \in UnifOn (X) \land M \subseteq X \times X) \land (V \in U \land V^{-1} = V)) \to cls (J \times_{t} J) (M) \subseteq V \circ (M \circ V)$

Metamath Proof Explorer

Theorem utop3cls

Proof