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	⊢ 𝐽 = ( unifTop ‘ 𝑈 )
	Assertion	utop3cls	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ) → ( ( cls ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ 𝑀 ) ⊆ ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) )

Proof

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

Metamath Proof Explorer

Theorem utop3cls

Proof