utop2nei - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > utop2nei		Structured version Visualization version GIF version

Theorem utop2nei 24624

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

**Hypothesis**
Ref	Expression
utoptop.1	⊢ 𝐽 = (unifTop‘𝑈)

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

Proof of Theorem utop2nei Dummy variables 𝑟 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		utoptop.1	. . . . . . . 8 ⊢ 𝐽 = (unifTop‘𝑈)
2		utoptop 24608	. . . . . . . 8 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ∈ Top)
3	1, 2	eqeltrid 2868	. . . . . . 7 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 ∈ Top)
4		txtop 23943	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝐽 ×_t 𝐽) ∈ Top)
5	3, 3, 4	syl2anc 596	. . . . . 6 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐽 ×_t 𝐽) ∈ Top)
6	5	3ad2ant1 1151	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → (𝐽 ×_t 𝐽) ∈ Top)
7	6	adantr 486	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 = ∅) → (𝐽 ×_t 𝐽) ∈ Top)
8		0nei 23501	. . . 4 ⊢ ((𝐽 ×_t 𝐽) ∈ Top → ∅ ∈ ((nei‘(𝐽 ×_t 𝐽))‘∅))
9	7, 8	syl 18	. . 3 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 = ∅) → ∅ ∈ ((nei‘(𝐽 ×_t 𝐽))‘∅))
10		coeq1 5846	. . . . . . 7 ⊢ (𝑀 = ∅ → (𝑀 ∘ 𝑉) = (∅ ∘ 𝑉))
11		co01 6284	. . . . . . 7 ⊢ (∅ ∘ 𝑉) = ∅
12	10, 11	eqtrdi 2814	. . . . . 6 ⊢ (𝑀 = ∅ → (𝑀 ∘ 𝑉) = ∅)
13	12	coeq2d 5851	. . . . 5 ⊢ (𝑀 = ∅ → (𝑉 ∘ (𝑀 ∘ 𝑉)) = (𝑉 ∘ ∅))
14		co02 6283	. . . . 5 ⊢ (𝑉 ∘ ∅) = ∅
15	13, 14	eqtrdi 2814	. . . 4 ⊢ (𝑀 = ∅ → (𝑉 ∘ (𝑀 ∘ 𝑉)) = ∅)
16	15	adantl 487	. . 3 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 = ∅) → (𝑉 ∘ (𝑀 ∘ 𝑉)) = ∅)
17		simpr 490	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 = ∅) → 𝑀 = ∅)
18	17	fveq2d 6920	. . 3 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 = ∅) → ((nei‘(𝐽 ×_t 𝐽))‘𝑀) = ((nei‘(𝐽 ×_t 𝐽))‘∅))
19	9, 16, 18	3eltr4d 2879	. 2 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 = ∅) → (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×_t 𝐽))‘𝑀))
20	6	adantr 486	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → (𝐽 ×_t 𝐽) ∈ Top)
21		simpl1 1210	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → 𝑈 ∈ (UnifOn‘𝑋))
22	21, 3	syl 18	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → 𝐽 ∈ Top)
23		simpl2l 1245	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → 𝑉 ∈ 𝑈)
24		simp3 1156	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → 𝑀 ⊆ (𝑋 × 𝑋))
25	24	sselda 3913	. . . . . . . . . . 11 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → 𝑟 ∈ (𝑋 × 𝑋))
26		xp1st 8067	. . . . . . . . . . 11 ⊢ (𝑟 ∈ (𝑋 × 𝑋) → (1^st ‘𝑟) ∈ 𝑋)
27	25, 26	syl 18	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → (1^st ‘𝑟) ∈ 𝑋)
28	1	utopsnnei 24623	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ (1^st ‘𝑟) ∈ 𝑋) → (𝑉 “ {(1^st ‘𝑟)}) ∈ ((nei‘𝐽)‘{(1^st ‘𝑟)}))
29	21, 23, 27, 28	syl3anc 1399	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → (𝑉 “ {(1^st ‘𝑟)}) ∈ ((nei‘𝐽)‘{(1^st ‘𝑟)}))
30		xp2nd 8068	. . . . . . . . . . 11 ⊢ (𝑟 ∈ (𝑋 × 𝑋) → (2^nd ‘𝑟) ∈ 𝑋)
31	25, 30	syl 18	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → (2^nd ‘𝑟) ∈ 𝑋)
32	1	utopsnnei 24623	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ (2^nd ‘𝑟) ∈ 𝑋) → (𝑉 “ {(2^nd ‘𝑟)}) ∈ ((nei‘𝐽)‘{(2^nd ‘𝑟)}))
33	21, 23, 31, 32	syl3anc 1399	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → (𝑉 “ {(2^nd ‘𝑟)}) ∈ ((nei‘𝐽)‘{(2^nd ‘𝑟)}))
34		eqid 2763	. . . . . . . . . 10 ⊢ ∪ 𝐽 = ∪ 𝐽
35	34, 34	neitx 23981	. . . . . . . . 9 ⊢ (((𝐽 ∈ 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 852	. . . . . . . 8 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)})) ∈ ((nei‘(𝐽 ×_t 𝐽))‘({(1^st ‘𝑟)} × {(2^nd ‘𝑟)})))
37		fvex 6929	. . . . . . . . . 10 ⊢ (1^st ‘𝑟) ∈ V
38		fvex 6929	. . . . . . . . . 10 ⊢ (2^nd ‘𝑟) ∈ V
39	37, 38	xpsn 7173	. . . . . . . . 9 ⊢ ({(1^st ‘𝑟)} × {(2^nd ‘𝑟)}) = {⟨(1^st ‘𝑟), (2^nd ‘𝑟)⟩}
40	39	fveq2i 6919	. . . . . . . 8 ⊢ ((nei‘(𝐽 ×_t 𝐽))‘({(1^st ‘𝑟)} × {(2^nd ‘𝑟)})) = ((nei‘(𝐽 ×_t 𝐽))‘{⟨(1^st ‘𝑟), (2^nd ‘𝑟)⟩})
41	36, 40	eleqtrdi 2874	. . . . . . 7 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)})) ∈ ((nei‘(𝐽 ×_t 𝐽))‘{⟨(1^st ‘𝑟), (2^nd ‘𝑟)⟩}))
42	24	adantr 486	. . . . . . . . . . 11 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → 𝑀 ⊆ (𝑋 × 𝑋))
43		xpss 5674	. . . . . . . . . . . . 13 ⊢ (𝑋 × 𝑋) ⊆ (V × V)
44		sstr 3921	. . . . . . . . . . . . 13 ⊢ ((𝑀 ⊆ (𝑋 × 𝑋) ∧ (𝑋 × 𝑋) ⊆ (V × V)) → 𝑀 ⊆ (V × V))
45	43, 44	mpan2 704	. . . . . . . . . . . 12 ⊢ (𝑀 ⊆ (𝑋 × 𝑋) → 𝑀 ⊆ (V × V))
46		df-rel 5665	. . . . . . . . . . . 12 ⊢ (Rel 𝑀 ↔ 𝑀 ⊆ (V × V))
47	45, 46	sylibr 237	. . . . . . . . . . 11 ⊢ (𝑀 ⊆ (𝑋 × 𝑋) → Rel 𝑀)
48	42, 47	syl 18	. . . . . . . . . 10 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → Rel 𝑀)
49		1st2nd 8084	. . . . . . . . . 10 ⊢ ((Rel 𝑀 ∧ 𝑟 ∈ 𝑀) → 𝑟 = ⟨(1^st ‘𝑟), (2^nd ‘𝑟)⟩)
50	48, 49	sylancom 600	. . . . . . . . 9 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → 𝑟 = ⟨(1^st ‘𝑟), (2^nd ‘𝑟)⟩)
51	50	sneqd 4596	. . . . . . . 8 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → {𝑟} = {⟨(1^st ‘𝑟), (2^nd ‘𝑟)⟩})
52	51	fveq2d 6920	. . . . . . 7 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → ((nei‘(𝐽 ×_t 𝐽))‘{𝑟}) = ((nei‘(𝐽 ×_t 𝐽))‘{⟨(1^st ‘𝑟), (2^nd ‘𝑟)⟩}))
53	41, 52	eleqtrrd 2867	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)})) ∈ ((nei‘(𝐽 ×_t 𝐽))‘{𝑟}))
54		relxp 5676	. . . . . . . . . . 11 ⊢ Rel ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)}))
55	54	a1i 11	. . . . . . . . . 10 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)}))) → Rel ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)})))
56		1st2nd 8084	. . . . . . . . . 10 ⊢ ((Rel ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)})) ∧ 𝑧 ∈ ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)}))) → 𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
57	55, 56	sylancom 600	. . . . . . . . 9 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)}))) → 𝑧 = ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩)
58		simpll2 1232	. . . . . . . . . . . . 13 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)}))) → (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉))
59	58	simprd 501	. . . . . . . . . . . 12 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)}))) → ^◡𝑉 = 𝑉)
60		simpll1 1231	. . . . . . . . . . . . . 14 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)}))) → 𝑈 ∈ (UnifOn‘𝑋))
61	58	simpld 500	. . . . . . . . . . . . . 14 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)}))) → 𝑉 ∈ 𝑈)
62		ustrel 24586	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → Rel 𝑉)
63	60, 61, 62	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)}))) → Rel 𝑉)
64		xp1st 8067	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)})) → (1^st ‘𝑧) ∈ (𝑉 “ {(1^st ‘𝑟)}))
65	64	adantl 487	. . . . . . . . . . . . 13 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)}))) → (1^st ‘𝑧) ∈ (𝑉 “ {(1^st ‘𝑟)}))
66		elrelimasn 6102	. . . . . . . . . . . . . 14 ⊢ (Rel 𝑉 → ((1^st ‘𝑧) ∈ (𝑉 “ {(1^st ‘𝑟)}) ↔ (1^st ‘𝑟)𝑉(1^st ‘𝑧)))
67	66	biimpa 482	. . . . . . . . . . . . 13 ⊢ ((Rel 𝑉 ∧ (1^st ‘𝑧) ∈ (𝑉 “ {(1^st ‘𝑟)})) → (1^st ‘𝑟)𝑉(1^st ‘𝑧))
68	63, 65, 67	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)}))) → (1^st ‘𝑟)𝑉(1^st ‘𝑧))
69		fvex 6929	. . . . . . . . . . . . . . 15 ⊢ (1^st ‘𝑧) ∈ V
70	37, 69	brcnv 5872	. . . . . . . . . . . . . 14 ⊢ ((1^st ‘𝑟)^◡𝑉(1^st ‘𝑧) ↔ (1^st ‘𝑧)𝑉(1^st ‘𝑟))
71		breq 5110	. . . . . . . . . . . . . 14 ⊢ (^◡𝑉 = 𝑉 → ((1^st ‘𝑟)^◡𝑉(1^st ‘𝑧) ↔ (1^st ‘𝑟)𝑉(1^st ‘𝑧)))
72	70, 71	bitr3id 288	. . . . . . . . . . . . 13 ⊢ (^◡𝑉 = 𝑉 → ((1^st ‘𝑧)𝑉(1^st ‘𝑟) ↔ (1^st ‘𝑟)𝑉(1^st ‘𝑧)))
73	72	biimpar 483	. . . . . . . . . . . 12 ⊢ ((^◡𝑉 = 𝑉 ∧ (1^st ‘𝑟)𝑉(1^st ‘𝑧)) → (1^st ‘𝑧)𝑉(1^st ‘𝑟))
74	59, 68, 73	syl2anc 596	. . . . . . . . . . 11 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)}))) → (1^st ‘𝑧)𝑉(1^st ‘𝑟))
75		simpll3 1233	. . . . . . . . . . . 12 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)}))) → 𝑀 ⊆ (𝑋 × 𝑋))
76		simplr 781	. . . . . . . . . . . 12 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)}))) → 𝑟 ∈ 𝑀)
77		1st2ndbr 8087	. . . . . . . . . . . . 13 ⊢ ((Rel 𝑀 ∧ 𝑟 ∈ 𝑀) → (1^st ‘𝑟)𝑀(2^nd ‘𝑟))
78	47, 77	sylan 592	. . . . . . . . . . . 12 ⊢ ((𝑀 ⊆ (𝑋 × 𝑋) ∧ 𝑟 ∈ 𝑀) → (1^st ‘𝑟)𝑀(2^nd ‘𝑟))
79	75, 76, 78	syl2anc 596	. . . . . . . . . . 11 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)}))) → (1^st ‘𝑟)𝑀(2^nd ‘𝑟))
80		xp2nd 8068	. . . . . . . . . . . . 13 ⊢ (𝑧 ∈ ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)})) → (2^nd ‘𝑧) ∈ (𝑉 “ {(2^nd ‘𝑟)}))
81	80	adantl 487	. . . . . . . . . . . 12 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)}))) → (2^nd ‘𝑧) ∈ (𝑉 “ {(2^nd ‘𝑟)}))
82		elrelimasn 6102	. . . . . . . . . . . . 13 ⊢ (Rel 𝑉 → ((2^nd ‘𝑧) ∈ (𝑉 “ {(2^nd ‘𝑟)}) ↔ (2^nd ‘𝑟)𝑉(2^nd ‘𝑧)))
83	82	biimpa 482	. . . . . . . . . . . 12 ⊢ ((Rel 𝑉 ∧ (2^nd ‘𝑧) ∈ (𝑉 “ {(2^nd ‘𝑟)})) → (2^nd ‘𝑟)𝑉(2^nd ‘𝑧))
84	63, 81, 83	syl2anc 596	. . . . . . . . . . 11 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)}))) → (2^nd ‘𝑟)𝑉(2^nd ‘𝑧))
85	69, 37, 38	brcoi 5858	. . . . . . . . . . . 12 ⊢ (((1^st ‘𝑧)𝑉(1^st ‘𝑟) ∧ (1^st ‘𝑟)𝑀(2^nd ‘𝑟)) → (1^st ‘𝑧)(𝑀 ∘ 𝑉)(2^nd ‘𝑟))
86		fvex 6929	. . . . . . . . . . . . 13 ⊢ (2^nd ‘𝑧) ∈ V
87	69, 38, 86	brcoi 5858	. . . . . . . . . . . 12 ⊢ (((1^st ‘𝑧)(𝑀 ∘ 𝑉)(2^nd ‘𝑟) ∧ (2^nd ‘𝑟)𝑉(2^nd ‘𝑧)) → (1^st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2^nd ‘𝑧))
88	85, 87	sylan 592	. . . . . . . . . . 11 ⊢ ((((1^st ‘𝑧)𝑉(1^st ‘𝑟) ∧ (1^st ‘𝑟)𝑀(2^nd ‘𝑟)) ∧ (2^nd ‘𝑟)𝑉(2^nd ‘𝑧)) → (1^st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2^nd ‘𝑧))
89	74, 79, 84, 88	syl21anc 851	. . . . . . . . . 10 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)}))) → (1^st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2^nd ‘𝑧))
90		df-br 5109	. . . . . . . . . 10 ⊢ ((1^st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2^nd ‘𝑧) ↔ ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∈ (𝑉 ∘ (𝑀 ∘ 𝑉)))
91	89, 90	sylib 221	. . . . . . . . 9 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)}))) → ⟨(1^st ‘𝑧), (2^nd ‘𝑧)⟩ ∈ (𝑉 ∘ (𝑀 ∘ 𝑉)))
92	57, 91	eqeltrd 2864	. . . . . . . 8 ⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) ∧ 𝑧 ∈ ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)}))) → 𝑧 ∈ (𝑉 ∘ (𝑀 ∘ 𝑉)))
93	92	ex 418	. . . . . . 7 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → (𝑧 ∈ ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)})) → 𝑧 ∈ (𝑉 ∘ (𝑀 ∘ 𝑉))))
94	93	ssrdv 3919	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)})) ⊆ (𝑉 ∘ (𝑀 ∘ 𝑉)))
95		simp1 1154	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → 𝑈 ∈ (UnifOn‘𝑋))
96		simp2l 1218	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → 𝑉 ∈ 𝑈)
97		ustssxp 24579	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → 𝑉 ⊆ (𝑋 × 𝑋))
98	95, 96, 97	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → 𝑉 ⊆ (𝑋 × 𝑋))
99		coss1 5843	. . . . . . . . . 10 ⊢ (𝑉 ⊆ (𝑋 × 𝑋) → (𝑉 ∘ (𝑀 ∘ 𝑉)) ⊆ ((𝑋 × 𝑋) ∘ (𝑀 ∘ 𝑉)))
100	98, 99	syl 18	. . . . . . . . 9 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → (𝑉 ∘ (𝑀 ∘ 𝑉)) ⊆ ((𝑋 × 𝑋) ∘ (𝑀 ∘ 𝑉)))
101		coss1 5843	. . . . . . . . . . . 12 ⊢ (𝑀 ⊆ (𝑋 × 𝑋) → (𝑀 ∘ 𝑉) ⊆ ((𝑋 × 𝑋) ∘ 𝑉))
102	24, 101	syl 18	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → (𝑀 ∘ 𝑉) ⊆ ((𝑋 × 𝑋) ∘ 𝑉))
103		coss2 5844	. . . . . . . . . . . . 13 ⊢ (𝑉 ⊆ (𝑋 × 𝑋) → ((𝑋 × 𝑋) ∘ 𝑉) ⊆ ((𝑋 × 𝑋) ∘ (𝑋 × 𝑋)))
104		xpcoid 6319	. . . . . . . . . . . . 13 ⊢ ((𝑋 × 𝑋) ∘ (𝑋 × 𝑋)) = (𝑋 × 𝑋)
105	103, 104	sseqtrdi 3953	. . . . . . . . . . . 12 ⊢ (𝑉 ⊆ (𝑋 × 𝑋) → ((𝑋 × 𝑋) ∘ 𝑉) ⊆ (𝑋 × 𝑋))
106	98, 105	syl 18	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → ((𝑋 × 𝑋) ∘ 𝑉) ⊆ (𝑋 × 𝑋))
107	102, 106	sstrd 3923	. . . . . . . . . 10 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → (𝑀 ∘ 𝑉) ⊆ (𝑋 × 𝑋))
108		coss2 5844	. . . . . . . . . . 11 ⊢ ((𝑀 ∘ 𝑉) ⊆ (𝑋 × 𝑋) → ((𝑋 × 𝑋) ∘ (𝑀 ∘ 𝑉)) ⊆ ((𝑋 × 𝑋) ∘ (𝑋 × 𝑋)))
109	108, 104	sseqtrdi 3953	. . . . . . . . . 10 ⊢ ((𝑀 ∘ 𝑉) ⊆ (𝑋 × 𝑋) → ((𝑋 × 𝑋) ∘ (𝑀 ∘ 𝑉)) ⊆ (𝑋 × 𝑋))
110	107, 109	syl 18	. . . . . . . . 9 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → ((𝑋 × 𝑋) ∘ (𝑀 ∘ 𝑉)) ⊆ (𝑋 × 𝑋))
111	100, 110	sstrd 3923	. . . . . . . 8 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → (𝑉 ∘ (𝑀 ∘ 𝑉)) ⊆ (𝑋 × 𝑋))
112		utopbas 24609	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = ∪ (unifTop‘𝑈))
113	1	unieqi 4884	. . . . . . . . . . . 12 ⊢ ∪ 𝐽 = ∪ (unifTop‘𝑈)
114	112, 113	eqtr4di 2816	. . . . . . . . . . 11 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = ∪ 𝐽)
115	114	sqxpeqd 5690	. . . . . . . . . 10 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) = (∪ 𝐽 × ∪ 𝐽))
116	34, 34	txuni 23966	. . . . . . . . . . 11 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (∪ 𝐽 × ∪ 𝐽) = ∪ (𝐽 ×_t 𝐽))
117	3, 3, 116	syl2anc 596	. . . . . . . . . 10 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (∪ 𝐽 × ∪ 𝐽) = ∪ (𝐽 ×_t 𝐽))
118	115, 117	eqtrd 2798	. . . . . . . . 9 ⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) = ∪ (𝐽 ×_t 𝐽))
119	118	3ad2ant1 1151	. . . . . . . 8 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → (𝑋 × 𝑋) = ∪ (𝐽 ×_t 𝐽))
120	111, 119	sseqtrd 3949	. . . . . . 7 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → (𝑉 ∘ (𝑀 ∘ 𝑉)) ⊆ ∪ (𝐽 ×_t 𝐽))
121	120	adantr 486	. . . . . 6 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → (𝑉 ∘ (𝑀 ∘ 𝑉)) ⊆ ∪ (𝐽 ×_t 𝐽))
122		eqid 2763	. . . . . . 7 ⊢ ∪ (𝐽 ×_t 𝐽) = ∪ (𝐽 ×_t 𝐽)
123	122	ssnei2 23489	. . . . . 6 ⊢ ((((𝐽 ×_t 𝐽) ∈ Top ∧ ((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)})) ∈ ((nei‘(𝐽 ×_t 𝐽))‘{𝑟})) ∧ (((𝑉 “ {(1^st ‘𝑟)}) × (𝑉 “ {(2^nd ‘𝑟)})) ⊆ (𝑉 ∘ (𝑀 ∘ 𝑉)) ∧ (𝑉 ∘ (𝑀 ∘ 𝑉)) ⊆ ∪ (𝐽 ×_t 𝐽))) → (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×_t 𝐽))‘{𝑟}))
124	20, 53, 94, 121, 123	syl22anc 852	. . . . 5 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑟 ∈ 𝑀) → (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×_t 𝐽))‘{𝑟}))
125	124	ralrimiva 3158	. . . 4 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → ∀𝑟 ∈ 𝑀 (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×_t 𝐽))‘{𝑟}))
126	125	adantr 486	. . 3 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 ≠ ∅) → ∀𝑟 ∈ 𝑀 (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×_t 𝐽))‘{𝑟}))
127	6	adantr 486	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 ≠ ∅) → (𝐽 ×_t 𝐽) ∈ Top)
128	24, 119	sseqtrd 3949	. . . . 5 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → 𝑀 ⊆ ∪ (𝐽 ×_t 𝐽))
129	128	adantr 486	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 ≠ ∅) → 𝑀 ⊆ ∪ (𝐽 ×_t 𝐽))
130		simpr 490	. . . 4 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 ≠ ∅) → 𝑀 ≠ ∅)
131	122	neips 23486	. . . 4 ⊢ (((𝐽 ×_t 𝐽) ∈ Top ∧ 𝑀 ⊆ ∪ (𝐽 ×_t 𝐽) ∧ 𝑀 ≠ ∅) → ((𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×_t 𝐽))‘𝑀) ↔ ∀𝑟 ∈ 𝑀 (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×_t 𝐽))‘{𝑟})))
132	127, 129, 130, 131	syl3anc 1399	. . 3 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 ≠ ∅) → ((𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×_t 𝐽))‘𝑀) ↔ ∀𝑟 ∈ 𝑀 (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×_t 𝐽))‘{𝑟})))
133	126, 132	mpbird 260	. 2 ⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ 𝑀 ≠ ∅) → (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×_t 𝐽))‘𝑀))
134	19, 133	pm2.61dane 3046	1 ⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ (𝑉 ∈ 𝑈 ∧ ^◡𝑉 = 𝑉) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) → (𝑉 ∘ (𝑀 ∘ 𝑉)) ∈ ((nei‘(𝐽 ×_t 𝐽))‘𝑀))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 Vcvv 3454 ⊆ wss 3900 ∅c0 4281 {csn 4588 ⟨cop 4840 ∪ cuni 4872 class class class wbr 5108 × cxp 5656 ^◡ccnv 5657 “ cima 5661 ∘ ccom 5662 Rel wrel 5663 ‘cfv 6566 (class class class)co 7451 1^st c1st 8033 2^nd c2nd 8034 Topctop 23266 neicnei 23470 ×_t ctx 23934 UnifOncust 24574 unifTopcutop 24604

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4841 df-uni 4873 df-int 4913 df-iun 4958 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-ov 7454 df-oprab 7455 df-mpo 7456 df-om 7912 df-1st 8035 df-2nd 8036 df-1o 8514 df-2o 8515 df-en 9012 df-fin 9015 df-fi 9440 df-topgen 17664 df-top 23267 df-topon 23284 df-bases 23319 df-nei 23471 df-tx 23936 df-ust 24575 df-utop 24605

This theorem is used by: (None)

W3C validator