utop2nei

Description: For any symmetrical entourage V and any relation M , build a neighborhood of M . First part of proposition 2 of BourbakiTop1 p. II.4. (Contributed by Thierry Arnoux, 14-Jan-2018)

		Ref	Expression
	Hypothesis	utoptop.1	⊢ 𝐽 = ( unifTop ‘ 𝑈 )
	Assertion	utop2nei	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) → ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ∈ ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		utoptop.1	⊢ 𝐽 = ( unifTop ‘ 𝑈 )
2		utoptop	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( unifTop ‘ 𝑈 ) ∈ Top )
3	1 2	eqeltrid	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝐽 ∈ Top )
4		txtop	⊢ ( ( 𝐽 ∈ Top ∧ 𝐽 ∈ Top ) → ( 𝐽 ×_t 𝐽 ) ∈ Top )
5	3 3 4	syl2anc	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐽 ×_t 𝐽 ) ∈ Top )
6	5	3ad2ant1	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) → ( 𝐽 ×_t 𝐽 ) ∈ Top )
7	6	adantr	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑀 = ∅ ) → ( 𝐽 ×_t 𝐽 ) ∈ Top )
8		0nei	⊢ ( ( 𝐽 ×_t 𝐽 ) ∈ Top → ∅ ∈ ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ ∅ ) )
9	7 8	syl	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑀 = ∅ ) → ∅ ∈ ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ ∅ ) )
10		coeq1	⊢ ( 𝑀 = ∅ → ( 𝑀 ∘ 𝑉 ) = ( ∅ ∘ 𝑉 ) )
11		co01	⊢ ( ∅ ∘ 𝑉 ) = ∅
12	10 11	eqtrdi	⊢ ( 𝑀 = ∅ → ( 𝑀 ∘ 𝑉 ) = ∅ )
13	12	coeq2d	⊢ ( 𝑀 = ∅ → ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) = ( 𝑉 ∘ ∅ ) )
14		co02	⊢ ( 𝑉 ∘ ∅ ) = ∅
15	13 14	eqtrdi	⊢ ( 𝑀 = ∅ → ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) = ∅ )
16	15	adantl	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑀 = ∅ ) → ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) = ∅ )
17		simpr	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑀 = ∅ ) → 𝑀 = ∅ )
18	17	fveq2d	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑀 = ∅ ) → ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ 𝑀 ) = ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ ∅ ) )
19	9 16 18	3eltr4d	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑀 = ∅ ) → ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ∈ ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ 𝑀 ) )
20	6	adantr	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) → ( 𝐽 ×_t 𝐽 ) ∈ Top )
21		simpl1	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
22	21 3	syl	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) → 𝐽 ∈ Top )
23		simpl2l	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) → 𝑉 ∈ 𝑈 )
24		simp3	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) → 𝑀 ⊆ ( 𝑋 × 𝑋 ) )
25	24	sselda	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) → 𝑟 ∈ ( 𝑋 × 𝑋 ) )
26		xp1st	⊢ ( 𝑟 ∈ ( 𝑋 × 𝑋 ) → ( 1^st ‘ 𝑟 ) ∈ 𝑋 )
27	25 26	syl	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) → ( 1^st ‘ 𝑟 ) ∈ 𝑋 )
28	1	utopsnnei	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ ( 1^st ‘ 𝑟 ) ∈ 𝑋 ) → ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { ( 1^st ‘ 𝑟 ) } ) )
29	21 23 27 28	syl3anc	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) → ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { ( 1^st ‘ 𝑟 ) } ) )
30		xp2nd	⊢ ( 𝑟 ∈ ( 𝑋 × 𝑋 ) → ( 2^nd ‘ 𝑟 ) ∈ 𝑋 )
31	25 30	syl	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) → ( 2^nd ‘ 𝑟 ) ∈ 𝑋 )
32	1	utopsnnei	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ ( 2^nd ‘ 𝑟 ) ∈ 𝑋 ) → ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { ( 2^nd ‘ 𝑟 ) } ) )
33	21 23 31 32	syl3anc	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) → ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { ( 2^nd ‘ 𝑟 ) } ) )
34		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
35	34 34	neitx	⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐽 ∈ Top ) ∧ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { ( 1^st ‘ 𝑟 ) } ) ∧ ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ∈ ( ( nei ‘ 𝐽 ) ‘ { ( 2^nd ‘ 𝑟 ) } ) ) ) → ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ∈ ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ ( { ( 1^st ‘ 𝑟 ) } × { ( 2^nd ‘ 𝑟 ) } ) ) )
36	22 22 29 33 35	syl22anc	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) → ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ∈ ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ ( { ( 1^st ‘ 𝑟 ) } × { ( 2^nd ‘ 𝑟 ) } ) ) )
37		fvex	⊢ ( 1^st ‘ 𝑟 ) ∈ V
38		fvex	⊢ ( 2^nd ‘ 𝑟 ) ∈ V
39	37 38	xpsn	⊢ ( { ( 1^st ‘ 𝑟 ) } × { ( 2^nd ‘ 𝑟 ) } ) = { ⟨ ( 1^st ‘ 𝑟 ) , ( 2^nd ‘ 𝑟 ) ⟩ }
40	39	fveq2i	⊢ ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ ( { ( 1^st ‘ 𝑟 ) } × { ( 2^nd ‘ 𝑟 ) } ) ) = ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ { ⟨ ( 1^st ‘ 𝑟 ) , ( 2^nd ‘ 𝑟 ) ⟩ } )
41	36 40	eleqtrdi	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) → ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ∈ ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ { ⟨ ( 1^st ‘ 𝑟 ) , ( 2^nd ‘ 𝑟 ) ⟩ } ) )
42	24	adantr	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) → 𝑀 ⊆ ( 𝑋 × 𝑋 ) )
43		xpss	⊢ ( 𝑋 × 𝑋 ) ⊆ ( V × V )
44		sstr	⊢ ( ( 𝑀 ⊆ ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ⊆ ( V × V ) ) → 𝑀 ⊆ ( V × V ) )
45	43 44	mpan2	⊢ ( 𝑀 ⊆ ( 𝑋 × 𝑋 ) → 𝑀 ⊆ ( V × V ) )
46		df-rel	⊢ ( Rel 𝑀 ↔ 𝑀 ⊆ ( V × V ) )
47	45 46	sylibr	⊢ ( 𝑀 ⊆ ( 𝑋 × 𝑋 ) → Rel 𝑀 )
48	42 47	syl	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) → Rel 𝑀 )
49		1st2nd	⊢ ( ( Rel 𝑀 ∧ 𝑟 ∈ 𝑀 ) → 𝑟 = ⟨ ( 1^st ‘ 𝑟 ) , ( 2^nd ‘ 𝑟 ) ⟩ )
50	48 49	sylancom	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) → 𝑟 = ⟨ ( 1^st ‘ 𝑟 ) , ( 2^nd ‘ 𝑟 ) ⟩ )
51	50	sneqd	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) → { 𝑟 } = { ⟨ ( 1^st ‘ 𝑟 ) , ( 2^nd ‘ 𝑟 ) ⟩ } )
52	51	fveq2d	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) → ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ { 𝑟 } ) = ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ { ⟨ ( 1^st ‘ 𝑟 ) , ( 2^nd ‘ 𝑟 ) ⟩ } ) )
53	41 52	eleqtrrd	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) → ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ∈ ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ { 𝑟 } ) )
54		relxp	⊢ Rel ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) )
55	54	a1i	⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) ∧ 𝑧 ∈ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ) → Rel ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) )
56		1st2nd	⊢ ( ( Rel ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ∧ 𝑧 ∈ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ) → 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
57	55 56	sylancom	⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) ∧ 𝑧 ∈ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ) → 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
58		simpll2	⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) ∧ 𝑧 ∈ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ) → ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) )
59	58	simprd	⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) ∧ 𝑧 ∈ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ) → ^◡ 𝑉 = 𝑉 )
60		simpll1	⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) ∧ 𝑧 ∈ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
61	58	simpld	⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) ∧ 𝑧 ∈ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ) → 𝑉 ∈ 𝑈 )
62		ustrel	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → Rel 𝑉 )
63	60 61 62	syl2anc	⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) ∧ 𝑧 ∈ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ) → Rel 𝑉 )
64		xp1st	⊢ ( 𝑧 ∈ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) → ( 1^st ‘ 𝑧 ) ∈ ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) )
65	64	adantl	⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) ∧ 𝑧 ∈ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ) → ( 1^st ‘ 𝑧 ) ∈ ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) )
66		elrelimasn	⊢ ( Rel 𝑉 → ( ( 1^st ‘ 𝑧 ) ∈ ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) ↔ ( 1^st ‘ 𝑟 ) 𝑉 ( 1^st ‘ 𝑧 ) ) )
67	66	biimpa	⊢ ( ( Rel 𝑉 ∧ ( 1^st ‘ 𝑧 ) ∈ ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) ) → ( 1^st ‘ 𝑟 ) 𝑉 ( 1^st ‘ 𝑧 ) )
68	63 65 67	syl2anc	⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) ∧ 𝑧 ∈ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ) → ( 1^st ‘ 𝑟 ) 𝑉 ( 1^st ‘ 𝑧 ) )
69		fvex	⊢ ( 1^st ‘ 𝑧 ) ∈ V
70	37 69	brcnv	⊢ ( ( 1^st ‘ 𝑟 ) ^◡ 𝑉 ( 1^st ‘ 𝑧 ) ↔ ( 1^st ‘ 𝑧 ) 𝑉 ( 1^st ‘ 𝑟 ) )
71		breq	⊢ ( ^◡ 𝑉 = 𝑉 → ( ( 1^st ‘ 𝑟 ) ^◡ 𝑉 ( 1^st ‘ 𝑧 ) ↔ ( 1^st ‘ 𝑟 ) 𝑉 ( 1^st ‘ 𝑧 ) ) )
72	70 71	bitr3id	⊢ ( ^◡ 𝑉 = 𝑉 → ( ( 1^st ‘ 𝑧 ) 𝑉 ( 1^st ‘ 𝑟 ) ↔ ( 1^st ‘ 𝑟 ) 𝑉 ( 1^st ‘ 𝑧 ) ) )
73	72	biimpar	⊢ ( ( ^◡ 𝑉 = 𝑉 ∧ ( 1^st ‘ 𝑟 ) 𝑉 ( 1^st ‘ 𝑧 ) ) → ( 1^st ‘ 𝑧 ) 𝑉 ( 1^st ‘ 𝑟 ) )
74	59 68 73	syl2anc	⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) ∧ 𝑧 ∈ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ) → ( 1^st ‘ 𝑧 ) 𝑉 ( 1^st ‘ 𝑟 ) )
75		simpll3	⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) ∧ 𝑧 ∈ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ) → 𝑀 ⊆ ( 𝑋 × 𝑋 ) )
76		simplr	⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) ∧ 𝑧 ∈ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ) → 𝑟 ∈ 𝑀 )
77		1st2ndbr	⊢ ( ( Rel 𝑀 ∧ 𝑟 ∈ 𝑀 ) → ( 1^st ‘ 𝑟 ) 𝑀 ( 2^nd ‘ 𝑟 ) )
78	47 77	sylan	⊢ ( ( 𝑀 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑟 ∈ 𝑀 ) → ( 1^st ‘ 𝑟 ) 𝑀 ( 2^nd ‘ 𝑟 ) )
79	75 76 78	syl2anc	⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) ∧ 𝑧 ∈ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ) → ( 1^st ‘ 𝑟 ) 𝑀 ( 2^nd ‘ 𝑟 ) )
80		xp2nd	⊢ ( 𝑧 ∈ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) → ( 2^nd ‘ 𝑧 ) ∈ ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) )
81	80	adantl	⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) ∧ 𝑧 ∈ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ) → ( 2^nd ‘ 𝑧 ) ∈ ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) )
82		elrelimasn	⊢ ( Rel 𝑉 → ( ( 2^nd ‘ 𝑧 ) ∈ ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ↔ ( 2^nd ‘ 𝑟 ) 𝑉 ( 2^nd ‘ 𝑧 ) ) )
83	82	biimpa	⊢ ( ( Rel 𝑉 ∧ ( 2^nd ‘ 𝑧 ) ∈ ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) → ( 2^nd ‘ 𝑟 ) 𝑉 ( 2^nd ‘ 𝑧 ) )
84	63 81 83	syl2anc	⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) ∧ 𝑧 ∈ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ) → ( 2^nd ‘ 𝑟 ) 𝑉 ( 2^nd ‘ 𝑧 ) )
85	69 38 37	3pm3.2i	⊢ ( ( 1^st ‘ 𝑧 ) ∈ V ∧ ( 2^nd ‘ 𝑟 ) ∈ V ∧ ( 1^st ‘ 𝑟 ) ∈ V )
86		brcogw	⊢ ( ( ( ( 1^st ‘ 𝑧 ) ∈ V ∧ ( 2^nd ‘ 𝑟 ) ∈ V ∧ ( 1^st ‘ 𝑟 ) ∈ V ) ∧ ( ( 1^st ‘ 𝑧 ) 𝑉 ( 1^st ‘ 𝑟 ) ∧ ( 1^st ‘ 𝑟 ) 𝑀 ( 2^nd ‘ 𝑟 ) ) ) → ( 1^st ‘ 𝑧 ) ( 𝑀 ∘ 𝑉 ) ( 2^nd ‘ 𝑟 ) )
87	85 86	mpan	⊢ ( ( ( 1^st ‘ 𝑧 ) 𝑉 ( 1^st ‘ 𝑟 ) ∧ ( 1^st ‘ 𝑟 ) 𝑀 ( 2^nd ‘ 𝑟 ) ) → ( 1^st ‘ 𝑧 ) ( 𝑀 ∘ 𝑉 ) ( 2^nd ‘ 𝑟 ) )
88		fvex	⊢ ( 2^nd ‘ 𝑧 ) ∈ V
89	69 88 38	3pm3.2i	⊢ ( ( 1^st ‘ 𝑧 ) ∈ V ∧ ( 2^nd ‘ 𝑧 ) ∈ V ∧ ( 2^nd ‘ 𝑟 ) ∈ V )
90		brcogw	⊢ ( ( ( ( 1^st ‘ 𝑧 ) ∈ V ∧ ( 2^nd ‘ 𝑧 ) ∈ V ∧ ( 2^nd ‘ 𝑟 ) ∈ V ) ∧ ( ( 1^st ‘ 𝑧 ) ( 𝑀 ∘ 𝑉 ) ( 2^nd ‘ 𝑟 ) ∧ ( 2^nd ‘ 𝑟 ) 𝑉 ( 2^nd ‘ 𝑧 ) ) ) → ( 1^st ‘ 𝑧 ) ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ( 2^nd ‘ 𝑧 ) )
91	89 90	mpan	⊢ ( ( ( 1^st ‘ 𝑧 ) ( 𝑀 ∘ 𝑉 ) ( 2^nd ‘ 𝑟 ) ∧ ( 2^nd ‘ 𝑟 ) 𝑉 ( 2^nd ‘ 𝑧 ) ) → ( 1^st ‘ 𝑧 ) ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ( 2^nd ‘ 𝑧 ) )
92	87 91	sylan	⊢ ( ( ( ( 1^st ‘ 𝑧 ) 𝑉 ( 1^st ‘ 𝑟 ) ∧ ( 1^st ‘ 𝑟 ) 𝑀 ( 2^nd ‘ 𝑟 ) ) ∧ ( 2^nd ‘ 𝑟 ) 𝑉 ( 2^nd ‘ 𝑧 ) ) → ( 1^st ‘ 𝑧 ) ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ( 2^nd ‘ 𝑧 ) )
93	74 79 84 92	syl21anc	⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) ∧ 𝑧 ∈ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ) → ( 1^st ‘ 𝑧 ) ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ( 2^nd ‘ 𝑧 ) )
94		df-br	⊢ ( ( 1^st ‘ 𝑧 ) ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ( 2^nd ‘ 𝑧 ) ↔ ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ∈ ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) )
95	93 94	sylib	⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) ∧ 𝑧 ∈ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ) → ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ∈ ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) )
96	57 95	eqeltrd	⊢ ( ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) ∧ 𝑧 ∈ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ) → 𝑧 ∈ ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) )
97	96	ex	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) → ( 𝑧 ∈ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) → 𝑧 ∈ ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ) )
98	97	ssrdv	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) → ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ⊆ ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) )
99		simp1	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
100		simp2l	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) → 𝑉 ∈ 𝑈 )
101		ustssxp	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → 𝑉 ⊆ ( 𝑋 × 𝑋 ) )
102	99 100 101	syl2anc	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) → 𝑉 ⊆ ( 𝑋 × 𝑋 ) )
103		coss1	⊢ ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) → ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ⊆ ( ( 𝑋 × 𝑋 ) ∘ ( 𝑀 ∘ 𝑉 ) ) )
104	102 103	syl	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) → ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ⊆ ( ( 𝑋 × 𝑋 ) ∘ ( 𝑀 ∘ 𝑉 ) ) )
105		coss1	⊢ ( 𝑀 ⊆ ( 𝑋 × 𝑋 ) → ( 𝑀 ∘ 𝑉 ) ⊆ ( ( 𝑋 × 𝑋 ) ∘ 𝑉 ) )
106	24 105	syl	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) → ( 𝑀 ∘ 𝑉 ) ⊆ ( ( 𝑋 × 𝑋 ) ∘ 𝑉 ) )
107		coss2	⊢ ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) → ( ( 𝑋 × 𝑋 ) ∘ 𝑉 ) ⊆ ( ( 𝑋 × 𝑋 ) ∘ ( 𝑋 × 𝑋 ) ) )
108		xpcoid	⊢ ( ( 𝑋 × 𝑋 ) ∘ ( 𝑋 × 𝑋 ) ) = ( 𝑋 × 𝑋 )
109	107 108	sseqtrdi	⊢ ( 𝑉 ⊆ ( 𝑋 × 𝑋 ) → ( ( 𝑋 × 𝑋 ) ∘ 𝑉 ) ⊆ ( 𝑋 × 𝑋 ) )
110	102 109	syl	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) → ( ( 𝑋 × 𝑋 ) ∘ 𝑉 ) ⊆ ( 𝑋 × 𝑋 ) )
111	106 110	sstrd	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) → ( 𝑀 ∘ 𝑉 ) ⊆ ( 𝑋 × 𝑋 ) )
112		coss2	⊢ ( ( 𝑀 ∘ 𝑉 ) ⊆ ( 𝑋 × 𝑋 ) → ( ( 𝑋 × 𝑋 ) ∘ ( 𝑀 ∘ 𝑉 ) ) ⊆ ( ( 𝑋 × 𝑋 ) ∘ ( 𝑋 × 𝑋 ) ) )
113	112 108	sseqtrdi	⊢ ( ( 𝑀 ∘ 𝑉 ) ⊆ ( 𝑋 × 𝑋 ) → ( ( 𝑋 × 𝑋 ) ∘ ( 𝑀 ∘ 𝑉 ) ) ⊆ ( 𝑋 × 𝑋 ) )
114	111 113	syl	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) → ( ( 𝑋 × 𝑋 ) ∘ ( 𝑀 ∘ 𝑉 ) ) ⊆ ( 𝑋 × 𝑋 ) )
115	104 114	sstrd	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) → ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ⊆ ( 𝑋 × 𝑋 ) )
116		utopbas	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = ∪ ( unifTop ‘ 𝑈 ) )
117	1	unieqi	⊢ ∪ 𝐽 = ∪ ( unifTop ‘ 𝑈 )
118	116 117	eqtr4di	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
119	118	sqxpeqd	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑋 × 𝑋 ) = ( ∪ 𝐽 × ∪ 𝐽 ) )
120	34 34	txuni	⊢ ( ( 𝐽 ∈ Top ∧ 𝐽 ∈ Top ) → ( ∪ 𝐽 × ∪ 𝐽 ) = ∪ ( 𝐽 ×_t 𝐽 ) )
121	3 3 120	syl2anc	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ∪ 𝐽 × ∪ 𝐽 ) = ∪ ( 𝐽 ×_t 𝐽 ) )
122	119 121	eqtrd	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑋 × 𝑋 ) = ∪ ( 𝐽 ×_t 𝐽 ) )
123	122	3ad2ant1	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) → ( 𝑋 × 𝑋 ) = ∪ ( 𝐽 ×_t 𝐽 ) )
124	115 123	sseqtrd	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) → ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ⊆ ∪ ( 𝐽 ×_t 𝐽 ) )
125	124	adantr	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) → ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ⊆ ∪ ( 𝐽 ×_t 𝐽 ) )
126		eqid	⊢ ∪ ( 𝐽 ×_t 𝐽 ) = ∪ ( 𝐽 ×_t 𝐽 )
127	126	ssnei2	⊢ ( ( ( ( 𝐽 ×_t 𝐽 ) ∈ Top ∧ ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ∈ ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ { 𝑟 } ) ) ∧ ( ( ( 𝑉 “ { ( 1^st ‘ 𝑟 ) } ) × ( 𝑉 “ { ( 2^nd ‘ 𝑟 ) } ) ) ⊆ ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ∧ ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ⊆ ∪ ( 𝐽 ×_t 𝐽 ) ) ) → ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ∈ ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ { 𝑟 } ) )
128	20 53 98 125 127	syl22anc	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑟 ∈ 𝑀 ) → ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ∈ ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ { 𝑟 } ) )
129	128	ralrimiva	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) → ∀ 𝑟 ∈ 𝑀 ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ∈ ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ { 𝑟 } ) )
130	129	adantr	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑀 ≠ ∅ ) → ∀ 𝑟 ∈ 𝑀 ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ∈ ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ { 𝑟 } ) )
131	6	adantr	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑀 ≠ ∅ ) → ( 𝐽 ×_t 𝐽 ) ∈ Top )
132	24 123	sseqtrd	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) → 𝑀 ⊆ ∪ ( 𝐽 ×_t 𝐽 ) )
133	132	adantr	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑀 ≠ ∅ ) → 𝑀 ⊆ ∪ ( 𝐽 ×_t 𝐽 ) )
134		simpr	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑀 ≠ ∅ ) → 𝑀 ≠ ∅ )
135	126	neips	⊢ ( ( ( 𝐽 ×_t 𝐽 ) ∈ Top ∧ 𝑀 ⊆ ∪ ( 𝐽 ×_t 𝐽 ) ∧ 𝑀 ≠ ∅ ) → ( ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ∈ ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ 𝑀 ) ↔ ∀ 𝑟 ∈ 𝑀 ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ∈ ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ { 𝑟 } ) ) )
136	131 133 134 135	syl3anc	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑀 ≠ ∅ ) → ( ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ∈ ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ 𝑀 ) ↔ ∀ 𝑟 ∈ 𝑀 ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ∈ ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ { 𝑟 } ) ) )
137	130 136	mpbird	⊢ ( ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) ∧ 𝑀 ≠ ∅ ) → ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ∈ ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ 𝑀 ) )
138	19 137	pm2.61dane	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ ( 𝑉 ∈ 𝑈 ∧ ^◡ 𝑉 = 𝑉 ) ∧ 𝑀 ⊆ ( 𝑋 × 𝑋 ) ) → ( 𝑉 ∘ ( 𝑀 ∘ 𝑉 ) ) ∈ ( ( nei ‘ ( 𝐽 ×_t 𝐽 ) ) ‘ 𝑀 ) )

Metamath Proof Explorer

Theorem utop2nei

Proof