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

Theorem utop3cls 23976
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.)
Hypothesis
Ref Expression
utoptop.1 𝐽 = (unifTopβ€˜π‘ˆ)
Assertion
Ref Expression
utop3cls (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) β†’ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€) βŠ† (𝑉 ∘ (𝑀 ∘ 𝑉)))

Proof of Theorem utop3cls
Dummy variables π‘Ÿ 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relxp 5693 . . . . 5 Rel (𝑋 Γ— 𝑋)
2 utoptop.1 . . . . . . . . . . 11 𝐽 = (unifTopβ€˜π‘ˆ)
3 utoptop 23959 . . . . . . . . . . 11 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ (unifTopβ€˜π‘ˆ) ∈ Top)
42, 3eqeltrid 2835 . . . . . . . . . 10 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ 𝐽 ∈ Top)
5 txtop 23293 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) β†’ (𝐽 Γ—t 𝐽) ∈ Top)
64, 4, 5syl2anc 582 . . . . . . . . 9 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ (𝐽 Γ—t 𝐽) ∈ Top)
76ad3antrrr 726 . . . . . . . 8 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) β†’ (𝐽 Γ—t 𝐽) ∈ Top)
8 simpllr 772 . . . . . . . . 9 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) β†’ 𝑀 βŠ† (𝑋 Γ— 𝑋))
9 utoptopon 23961 . . . . . . . . . . . . . 14 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ (unifTopβ€˜π‘ˆ) ∈ (TopOnβ€˜π‘‹))
102, 9eqeltrid 2835 . . . . . . . . . . . . 13 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
11 toponuni 22636 . . . . . . . . . . . . 13 (𝐽 ∈ (TopOnβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝐽)
1210, 11syl 17 . . . . . . . . . . . 12 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝐽)
1312sqxpeqd 5707 . . . . . . . . . . 11 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ (𝑋 Γ— 𝑋) = (βˆͺ 𝐽 Γ— βˆͺ 𝐽))
14 eqid 2730 . . . . . . . . . . . . 13 βˆͺ 𝐽 = βˆͺ 𝐽
1514, 14txuni 23316 . . . . . . . . . . . 12 ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) β†’ (βˆͺ 𝐽 Γ— βˆͺ 𝐽) = βˆͺ (𝐽 Γ—t 𝐽))
164, 4, 15syl2anc 582 . . . . . . . . . . 11 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ (βˆͺ 𝐽 Γ— βˆͺ 𝐽) = βˆͺ (𝐽 Γ—t 𝐽))
1713, 16eqtrd 2770 . . . . . . . . . 10 (π‘ˆ ∈ (UnifOnβ€˜π‘‹) β†’ (𝑋 Γ— 𝑋) = βˆͺ (𝐽 Γ—t 𝐽))
1817ad3antrrr 726 . . . . . . . . 9 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) β†’ (𝑋 Γ— 𝑋) = βˆͺ (𝐽 Γ—t 𝐽))
198, 18sseqtrd 4021 . . . . . . . 8 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) β†’ 𝑀 βŠ† βˆͺ (𝐽 Γ—t 𝐽))
20 eqid 2730 . . . . . . . . 9 βˆͺ (𝐽 Γ—t 𝐽) = βˆͺ (𝐽 Γ—t 𝐽)
2120clsss3 22783 . . . . . . . 8 (((𝐽 Γ—t 𝐽) ∈ Top ∧ 𝑀 βŠ† βˆͺ (𝐽 Γ—t 𝐽)) β†’ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€) βŠ† βˆͺ (𝐽 Γ—t 𝐽))
227, 19, 21syl2anc 582 . . . . . . 7 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) β†’ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€) βŠ† βˆͺ (𝐽 Γ—t 𝐽))
2322, 18sseqtrrd 4022 . . . . . 6 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) β†’ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€) βŠ† (𝑋 Γ— 𝑋))
24 simpr 483 . . . . . 6 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) β†’ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€))
2523, 24sseldd 3982 . . . . 5 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) β†’ 𝑧 ∈ (𝑋 Γ— 𝑋))
26 1st2nd 8027 . . . . 5 ((Rel (𝑋 Γ— 𝑋) ∧ 𝑧 ∈ (𝑋 Γ— 𝑋)) β†’ 𝑧 = ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩)
271, 25, 26sylancr 585 . . . 4 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) β†’ 𝑧 = ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩)
28 simp-4l 779 . . . . . . . . . 10 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) ∧ π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀)) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
29 simpr1l 1228 . . . . . . . . . . 11 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ ((𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€) ∧ π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀))) β†’ 𝑉 ∈ π‘ˆ)
30293anassrs 1358 . . . . . . . . . 10 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) ∧ π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀)) β†’ 𝑉 ∈ π‘ˆ)
31 ustrel 23936 . . . . . . . . . 10 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑉 ∈ π‘ˆ) β†’ Rel 𝑉)
3228, 30, 31syl2anc 582 . . . . . . . . 9 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) ∧ π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀)) β†’ Rel 𝑉)
33 simpr 483 . . . . . . . . . . . 12 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) ∧ π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀)) β†’ π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀))
34 elin 3963 . . . . . . . . . . . 12 (π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀) ↔ (π‘Ÿ ∈ ((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∧ π‘Ÿ ∈ 𝑀))
3533, 34sylib 217 . . . . . . . . . . 11 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) ∧ π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀)) β†’ (π‘Ÿ ∈ ((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∧ π‘Ÿ ∈ 𝑀))
3635simpld 493 . . . . . . . . . 10 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) ∧ π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀)) β†’ π‘Ÿ ∈ ((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})))
37 xp1st 8009 . . . . . . . . . 10 (π‘Ÿ ∈ ((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) β†’ (1st β€˜π‘Ÿ) ∈ (𝑉 β€œ {(1st β€˜π‘§)}))
3836, 37syl 17 . . . . . . . . 9 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) ∧ π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀)) β†’ (1st β€˜π‘Ÿ) ∈ (𝑉 β€œ {(1st β€˜π‘§)}))
39 elrelimasn 6083 . . . . . . . . . 10 (Rel 𝑉 β†’ ((1st β€˜π‘Ÿ) ∈ (𝑉 β€œ {(1st β€˜π‘§)}) ↔ (1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ)))
4039biimpa 475 . . . . . . . . 9 ((Rel 𝑉 ∧ (1st β€˜π‘Ÿ) ∈ (𝑉 β€œ {(1st β€˜π‘§)})) β†’ (1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ))
4132, 38, 40syl2anc 582 . . . . . . . 8 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) ∧ π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀)) β†’ (1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ))
42 simp-4r 780 . . . . . . . . . . 11 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) ∧ π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀)) β†’ 𝑀 βŠ† (𝑋 Γ— 𝑋))
43 xpss 5691 . . . . . . . . . . 11 (𝑋 Γ— 𝑋) βŠ† (V Γ— V)
4442, 43sstrdi 3993 . . . . . . . . . 10 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) ∧ π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀)) β†’ 𝑀 βŠ† (V Γ— V))
45 df-rel 5682 . . . . . . . . . 10 (Rel 𝑀 ↔ 𝑀 βŠ† (V Γ— V))
4644, 45sylibr 233 . . . . . . . . 9 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) ∧ π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀)) β†’ Rel 𝑀)
4735simprd 494 . . . . . . . . 9 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) ∧ π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀)) β†’ π‘Ÿ ∈ 𝑀)
48 1st2ndbr 8030 . . . . . . . . 9 ((Rel 𝑀 ∧ π‘Ÿ ∈ 𝑀) β†’ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ))
4946, 47, 48syl2anc 582 . . . . . . . 8 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) ∧ π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀)) β†’ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ))
50 xp2nd 8010 . . . . . . . . . . 11 (π‘Ÿ ∈ ((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) β†’ (2nd β€˜π‘Ÿ) ∈ (𝑉 β€œ {(2nd β€˜π‘§)}))
5136, 50syl 17 . . . . . . . . . 10 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) ∧ π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀)) β†’ (2nd β€˜π‘Ÿ) ∈ (𝑉 β€œ {(2nd β€˜π‘§)}))
52 elrelimasn 6083 . . . . . . . . . . 11 (Rel 𝑉 β†’ ((2nd β€˜π‘Ÿ) ∈ (𝑉 β€œ {(2nd β€˜π‘§)}) ↔ (2nd β€˜π‘§)𝑉(2nd β€˜π‘Ÿ)))
5352biimpa 475 . . . . . . . . . 10 ((Rel 𝑉 ∧ (2nd β€˜π‘Ÿ) ∈ (𝑉 β€œ {(2nd β€˜π‘§)})) β†’ (2nd β€˜π‘§)𝑉(2nd β€˜π‘Ÿ))
5432, 51, 53syl2anc 582 . . . . . . . . 9 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) ∧ π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀)) β†’ (2nd β€˜π‘§)𝑉(2nd β€˜π‘Ÿ))
55 simpr1r 1229 . . . . . . . . . . 11 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ ((𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€) ∧ π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀))) β†’ ◑𝑉 = 𝑉)
56553anassrs 1358 . . . . . . . . . 10 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) ∧ π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀)) β†’ ◑𝑉 = 𝑉)
57 breq 5149 . . . . . . . . . . 11 (◑𝑉 = 𝑉 β†’ ((2nd β€˜π‘Ÿ)◑𝑉(2nd β€˜π‘§) ↔ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§)))
58 fvex 6903 . . . . . . . . . . . 12 (2nd β€˜π‘Ÿ) ∈ V
59 fvex 6903 . . . . . . . . . . . 12 (2nd β€˜π‘§) ∈ V
6058, 59brcnv 5881 . . . . . . . . . . 11 ((2nd β€˜π‘Ÿ)◑𝑉(2nd β€˜π‘§) ↔ (2nd β€˜π‘§)𝑉(2nd β€˜π‘Ÿ))
6157, 60bitr3di 285 . . . . . . . . . 10 (◑𝑉 = 𝑉 β†’ ((2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§) ↔ (2nd β€˜π‘§)𝑉(2nd β€˜π‘Ÿ)))
6256, 61syl 17 . . . . . . . . 9 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) ∧ π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀)) β†’ ((2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§) ↔ (2nd β€˜π‘§)𝑉(2nd β€˜π‘Ÿ)))
6354, 62mpbird 256 . . . . . . . 8 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) ∧ π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀)) β†’ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§))
64 fvex 6903 . . . . . . . . . 10 (1st β€˜π‘§) ∈ V
65 fvex 6903 . . . . . . . . . 10 (1st β€˜π‘Ÿ) ∈ V
66 brcogw 5867 . . . . . . . . . . 11 ((((1st β€˜π‘§) ∈ V ∧ (2nd β€˜π‘Ÿ) ∈ V ∧ (1st β€˜π‘Ÿ) ∈ V) ∧ ((1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ) ∧ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ))) β†’ (1st β€˜π‘§)(𝑀 ∘ 𝑉)(2nd β€˜π‘Ÿ))
6766ex 411 . . . . . . . . . 10 (((1st β€˜π‘§) ∈ V ∧ (2nd β€˜π‘Ÿ) ∈ V ∧ (1st β€˜π‘Ÿ) ∈ V) β†’ (((1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ) ∧ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ)) β†’ (1st β€˜π‘§)(𝑀 ∘ 𝑉)(2nd β€˜π‘Ÿ)))
6864, 58, 65, 67mp3an 1459 . . . . . . . . 9 (((1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ) ∧ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ)) β†’ (1st β€˜π‘§)(𝑀 ∘ 𝑉)(2nd β€˜π‘Ÿ))
69 brcogw 5867 . . . . . . . . . . 11 ((((1st β€˜π‘§) ∈ V ∧ (2nd β€˜π‘§) ∈ V ∧ (2nd β€˜π‘Ÿ) ∈ V) ∧ ((1st β€˜π‘§)(𝑀 ∘ 𝑉)(2nd β€˜π‘Ÿ) ∧ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§))) β†’ (1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§))
7069ex 411 . . . . . . . . . 10 (((1st β€˜π‘§) ∈ V ∧ (2nd β€˜π‘§) ∈ V ∧ (2nd β€˜π‘Ÿ) ∈ V) β†’ (((1st β€˜π‘§)(𝑀 ∘ 𝑉)(2nd β€˜π‘Ÿ) ∧ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§)) β†’ (1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§)))
7164, 59, 58, 70mp3an 1459 . . . . . . . . 9 (((1st β€˜π‘§)(𝑀 ∘ 𝑉)(2nd β€˜π‘Ÿ) ∧ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§)) β†’ (1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§))
7268, 71sylan 578 . . . . . . . 8 ((((1st β€˜π‘§)𝑉(1st β€˜π‘Ÿ) ∧ (1st β€˜π‘Ÿ)𝑀(2nd β€˜π‘Ÿ)) ∧ (2nd β€˜π‘Ÿ)𝑉(2nd β€˜π‘§)) β†’ (1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§))
7341, 49, 63, 72syl21anc 834 . . . . . . 7 (((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) ∧ π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀)) β†’ (1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§))
7473ralrimiva 3144 . . . . . 6 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) β†’ βˆ€π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀)(1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§))
75 simplll 771 . . . . . . . . 9 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) β†’ π‘ˆ ∈ (UnifOnβ€˜π‘‹))
76 simplrl 773 . . . . . . . . 9 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) β†’ 𝑉 ∈ π‘ˆ)
7743ad2ant1 1131 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑉 ∈ π‘ˆ ∧ 𝑧 ∈ (𝑋 Γ— 𝑋)) β†’ 𝐽 ∈ Top)
78 xp1st 8009 . . . . . . . . . . . 12 (𝑧 ∈ (𝑋 Γ— 𝑋) β†’ (1st β€˜π‘§) ∈ 𝑋)
792utopsnnei 23974 . . . . . . . . . . . 12 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑉 ∈ π‘ˆ ∧ (1st β€˜π‘§) ∈ 𝑋) β†’ (𝑉 β€œ {(1st β€˜π‘§)}) ∈ ((neiβ€˜π½)β€˜{(1st β€˜π‘§)}))
8078, 79syl3an3 1163 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑉 ∈ π‘ˆ ∧ 𝑧 ∈ (𝑋 Γ— 𝑋)) β†’ (𝑉 β€œ {(1st β€˜π‘§)}) ∈ ((neiβ€˜π½)β€˜{(1st β€˜π‘§)}))
81 xp2nd 8010 . . . . . . . . . . . 12 (𝑧 ∈ (𝑋 Γ— 𝑋) β†’ (2nd β€˜π‘§) ∈ 𝑋)
822utopsnnei 23974 . . . . . . . . . . . 12 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑉 ∈ π‘ˆ ∧ (2nd β€˜π‘§) ∈ 𝑋) β†’ (𝑉 β€œ {(2nd β€˜π‘§)}) ∈ ((neiβ€˜π½)β€˜{(2nd β€˜π‘§)}))
8381, 82syl3an3 1163 . . . . . . . . . . 11 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑉 ∈ π‘ˆ ∧ 𝑧 ∈ (𝑋 Γ— 𝑋)) β†’ (𝑉 β€œ {(2nd β€˜π‘§)}) ∈ ((neiβ€˜π½)β€˜{(2nd β€˜π‘§)}))
8414, 14neitx 23331 . . . . . . . . . . 11 (((𝐽 ∈ Top ∧ 𝐽 ∈ Top) ∧ ((𝑉 β€œ {(1st β€˜π‘§)}) ∈ ((neiβ€˜π½)β€˜{(1st β€˜π‘§)}) ∧ (𝑉 β€œ {(2nd β€˜π‘§)}) ∈ ((neiβ€˜π½)β€˜{(2nd β€˜π‘§)}))) β†’ ((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜({(1st β€˜π‘§)} Γ— {(2nd β€˜π‘§)})))
8577, 77, 80, 83, 84syl22anc 835 . . . . . . . . . 10 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑉 ∈ π‘ˆ ∧ 𝑧 ∈ (𝑋 Γ— 𝑋)) β†’ ((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜({(1st β€˜π‘§)} Γ— {(2nd β€˜π‘§)})))
86 1st2nd2 8016 . . . . . . . . . . . . . 14 (𝑧 ∈ (𝑋 Γ— 𝑋) β†’ 𝑧 = ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩)
8786sneqd 4639 . . . . . . . . . . . . 13 (𝑧 ∈ (𝑋 Γ— 𝑋) β†’ {𝑧} = {⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩})
8864, 59xpsn 7140 . . . . . . . . . . . . 13 ({(1st β€˜π‘§)} Γ— {(2nd β€˜π‘§)}) = {⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩}
8987, 88eqtr4di 2788 . . . . . . . . . . . 12 (𝑧 ∈ (𝑋 Γ— 𝑋) β†’ {𝑧} = ({(1st β€˜π‘§)} Γ— {(2nd β€˜π‘§)}))
9089fveq2d 6894 . . . . . . . . . . 11 (𝑧 ∈ (𝑋 Γ— 𝑋) β†’ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{𝑧}) = ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜({(1st β€˜π‘§)} Γ— {(2nd β€˜π‘§)})))
91903ad2ant3 1133 . . . . . . . . . 10 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑉 ∈ π‘ˆ ∧ 𝑧 ∈ (𝑋 Γ— 𝑋)) β†’ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{𝑧}) = ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜({(1st β€˜π‘§)} Γ— {(2nd β€˜π‘§)})))
9285, 91eleqtrrd 2834 . . . . . . . . 9 ((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑉 ∈ π‘ˆ ∧ 𝑧 ∈ (𝑋 Γ— 𝑋)) β†’ ((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{𝑧}))
9375, 76, 25, 92syl3anc 1369 . . . . . . . 8 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) β†’ ((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{𝑧}))
9420neindisj 22841 . . . . . . . 8 ((((𝐽 Γ—t 𝐽) ∈ Top ∧ 𝑀 βŠ† βˆͺ (𝐽 Γ—t 𝐽)) ∧ (𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€) ∧ ((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∈ ((neiβ€˜(𝐽 Γ—t 𝐽))β€˜{𝑧}))) β†’ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀) β‰  βˆ…)
957, 19, 24, 93, 94syl22anc 835 . . . . . . 7 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) β†’ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀) β‰  βˆ…)
96 r19.3rzv 4497 . . . . . . 7 ((((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀) β‰  βˆ… β†’ ((1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§) ↔ βˆ€π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀)(1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§)))
9795, 96syl 17 . . . . . 6 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) β†’ ((1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§) ↔ βˆ€π‘Ÿ ∈ (((𝑉 β€œ {(1st β€˜π‘§)}) Γ— (𝑉 β€œ {(2nd β€˜π‘§)})) ∩ 𝑀)(1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§)))
9874, 97mpbird 256 . . . . 5 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) β†’ (1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§))
99 df-br 5148 . . . . 5 ((1st β€˜π‘§)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd β€˜π‘§) ↔ ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩ ∈ (𝑉 ∘ (𝑀 ∘ 𝑉)))
10098, 99sylib 217 . . . 4 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) β†’ ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩ ∈ (𝑉 ∘ (𝑀 ∘ 𝑉)))
10127, 100eqeltrd 2831 . . 3 ((((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) ∧ 𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€)) β†’ 𝑧 ∈ (𝑉 ∘ (𝑀 ∘ 𝑉)))
102101ex 411 . 2 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) β†’ (𝑧 ∈ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€) β†’ 𝑧 ∈ (𝑉 ∘ (𝑀 ∘ 𝑉))))
103102ssrdv 3987 1 (((π‘ˆ ∈ (UnifOnβ€˜π‘‹) ∧ 𝑀 βŠ† (𝑋 Γ— 𝑋)) ∧ (𝑉 ∈ π‘ˆ ∧ ◑𝑉 = 𝑉)) β†’ ((clsβ€˜(𝐽 Γ—t 𝐽))β€˜π‘€) βŠ† (𝑉 ∘ (𝑀 ∘ 𝑉)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104   β‰  wne 2938  βˆ€wral 3059  Vcvv 3472   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  {csn 4627  βŸ¨cop 4633  βˆͺ cuni 4907   class class class wbr 5147   Γ— cxp 5673  β—‘ccnv 5674   β€œ cima 5678   ∘ ccom 5679  Rel wrel 5680  β€˜cfv 6542  (class class class)co 7411  1st c1st 7975  2nd c2nd 7976  Topctop 22615  TopOnctopon 22632  clsccl 22742  neicnei 22821   Γ—t ctx 23284  UnifOncust 23924  unifTopcutop 23955
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-1o 8468  df-er 8705  df-en 8942  df-fin 8945  df-fi 9408  df-topgen 17393  df-top 22616  df-topon 22633  df-bases 22669  df-cld 22743  df-ntr 22744  df-cls 22745  df-nei 22822  df-tx 23286  df-ust 23925  df-utop 23956
This theorem is referenced by:  utopreg  23977
  Copyright terms: Public domain W3C validator