Step | Hyp | Ref
| Expression |
1 | | relxp 5150 |
. . . . 5
⊢ Rel
(𝑋 × 𝑋) |
2 | | utoptop.1 |
. . . . . . . . . . 11
⊢ 𝐽 = (unifTop‘𝑈) |
3 | | utoptop 21848 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ∈ Top) |
4 | 2, 3 | syl5eqel 2692 |
. . . . . . . . . 10
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 ∈ Top) |
5 | | txtop 21182 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (𝐽 ×t 𝐽) ∈ Top) |
6 | 4, 4, 5 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝐽 ×t 𝐽) ∈ Top) |
7 | 6 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → (𝐽 ×t 𝐽) ∈ Top) |
8 | | simpllr 795 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑀 ⊆ (𝑋 × 𝑋)) |
9 | | utoptopon 21850 |
. . . . . . . . . . . . . 14
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ∈ (TopOn‘𝑋)) |
10 | 2, 9 | syl5eqel 2692 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 ∈ (TopOn‘𝑋)) |
11 | | toponuni 20542 |
. . . . . . . . . . . . 13
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = ∪ 𝐽) |
13 | 12 | sqxpeqd 5065 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) = (∪ 𝐽 × ∪ 𝐽)) |
14 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ ∪ 𝐽 =
∪ 𝐽 |
15 | 14, 14 | txuni 21205 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ 𝐽 ∈ Top) → (∪ 𝐽
× ∪ 𝐽) = ∪ (𝐽 ×t 𝐽)) |
16 | 4, 4, 15 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (∪ 𝐽
× ∪ 𝐽) = ∪ (𝐽 ×t 𝐽)) |
17 | 13, 16 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽)) |
18 | 17 | ad3antrrr 762 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → (𝑋 × 𝑋) = ∪ (𝐽 ×t 𝐽)) |
19 | 8, 18 | sseqtrd 3604 |
. . . . . . . 8
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑀 ⊆ ∪ (𝐽 ×t 𝐽)) |
20 | | eqid 2610 |
. . . . . . . . 9
⊢ ∪ (𝐽
×t 𝐽) =
∪ (𝐽 ×t 𝐽) |
21 | 20 | clsss3 20673 |
. . . . . . . 8
⊢ (((𝐽 ×t 𝐽) ∈ Top ∧ 𝑀 ⊆ ∪ (𝐽
×t 𝐽))
→ ((cls‘(𝐽
×t 𝐽))‘𝑀) ⊆ ∪
(𝐽 ×t
𝐽)) |
22 | 7, 19, 21 | syl2anc 691 |
. . . . . . 7
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → ((cls‘(𝐽 ×t 𝐽))‘𝑀) ⊆ ∪
(𝐽 ×t
𝐽)) |
23 | 22, 18 | sseqtr4d 3605 |
. . . . . 6
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → ((cls‘(𝐽 ×t 𝐽))‘𝑀) ⊆ (𝑋 × 𝑋)) |
24 | | simpr 476 |
. . . . . 6
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) |
25 | 23, 24 | sseldd 3569 |
. . . . 5
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑧 ∈ (𝑋 × 𝑋)) |
26 | | 1st2nd 7105 |
. . . . 5
⊢ ((Rel
(𝑋 × 𝑋) ∧ 𝑧 ∈ (𝑋 × 𝑋)) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
27 | 1, 25, 26 | sylancr 694 |
. . . 4
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
28 | | simp-4l 802 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → 𝑈 ∈ (UnifOn‘𝑋)) |
29 | | simpr1l 1111 |
. . . . . . . . . . 11
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ ((𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀))) → 𝑉 ∈ 𝑈) |
30 | 29 | 3anassrs 1282 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → 𝑉 ∈ 𝑈) |
31 | | ustrel 21825 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈) → Rel 𝑉) |
32 | 28, 30, 31 | syl2anc 691 |
. . . . . . . . 9
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → Rel 𝑉) |
33 | | simpr 476 |
. . . . . . . . . . . 12
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) |
34 | | elin 3758 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀) ↔ (𝑟 ∈ ((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∧ 𝑟 ∈ 𝑀)) |
35 | 33, 34 | sylib 207 |
. . . . . . . . . . 11
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → (𝑟 ∈ ((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∧ 𝑟 ∈ 𝑀)) |
36 | 35 | simpld 474 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → 𝑟 ∈ ((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)}))) |
37 | | xp1st 7089 |
. . . . . . . . . 10
⊢ (𝑟 ∈ ((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) → (1st
‘𝑟) ∈ (𝑉 “ {(1st
‘𝑧)})) |
38 | 36, 37 | syl 17 |
. . . . . . . . 9
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → (1st ‘𝑟) ∈ (𝑉 “ {(1st ‘𝑧)})) |
39 | | elrelimasn 5408 |
. . . . . . . . . 10
⊢ (Rel
𝑉 → ((1st
‘𝑟) ∈ (𝑉 “ {(1st
‘𝑧)}) ↔
(1st ‘𝑧)𝑉(1st ‘𝑟))) |
40 | 39 | biimpa 500 |
. . . . . . . . 9
⊢ ((Rel
𝑉 ∧ (1st
‘𝑟) ∈ (𝑉 “ {(1st
‘𝑧)})) →
(1st ‘𝑧)𝑉(1st ‘𝑟)) |
41 | 32, 38, 40 | syl2anc 691 |
. . . . . . . 8
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → (1st ‘𝑧)𝑉(1st ‘𝑟)) |
42 | | simp-4r 803 |
. . . . . . . . . . 11
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → 𝑀 ⊆ (𝑋 × 𝑋)) |
43 | | xpss 5149 |
. . . . . . . . . . 11
⊢ (𝑋 × 𝑋) ⊆ (V × V) |
44 | 42, 43 | syl6ss 3580 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → 𝑀 ⊆ (V × V)) |
45 | | df-rel 5045 |
. . . . . . . . . 10
⊢ (Rel
𝑀 ↔ 𝑀 ⊆ (V × V)) |
46 | 44, 45 | sylibr 223 |
. . . . . . . . 9
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → Rel 𝑀) |
47 | 35 | simprd 478 |
. . . . . . . . 9
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → 𝑟 ∈ 𝑀) |
48 | | 1st2ndbr 7108 |
. . . . . . . . 9
⊢ ((Rel
𝑀 ∧ 𝑟 ∈ 𝑀) → (1st ‘𝑟)𝑀(2nd ‘𝑟)) |
49 | 46, 47, 48 | syl2anc 691 |
. . . . . . . 8
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → (1st ‘𝑟)𝑀(2nd ‘𝑟)) |
50 | | xp2nd 7090 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ ((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) → (2nd
‘𝑟) ∈ (𝑉 “ {(2nd
‘𝑧)})) |
51 | 36, 50 | syl 17 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → (2nd ‘𝑟) ∈ (𝑉 “ {(2nd ‘𝑧)})) |
52 | | elrelimasn 5408 |
. . . . . . . . . . 11
⊢ (Rel
𝑉 → ((2nd
‘𝑟) ∈ (𝑉 “ {(2nd
‘𝑧)}) ↔
(2nd ‘𝑧)𝑉(2nd ‘𝑟))) |
53 | 52 | biimpa 500 |
. . . . . . . . . 10
⊢ ((Rel
𝑉 ∧ (2nd
‘𝑟) ∈ (𝑉 “ {(2nd
‘𝑧)})) →
(2nd ‘𝑧)𝑉(2nd ‘𝑟)) |
54 | 32, 51, 53 | syl2anc 691 |
. . . . . . . . 9
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → (2nd ‘𝑧)𝑉(2nd ‘𝑟)) |
55 | | simpr1r 1112 |
. . . . . . . . . . 11
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ ((𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀))) → ◡𝑉 = 𝑉) |
56 | 55 | 3anassrs 1282 |
. . . . . . . . . 10
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → ◡𝑉 = 𝑉) |
57 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
(2nd ‘𝑟) ∈ V |
58 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
(2nd ‘𝑧) ∈ V |
59 | 57, 58 | brcnv 5227 |
. . . . . . . . . . 11
⊢
((2nd ‘𝑟)◡𝑉(2nd ‘𝑧) ↔ (2nd ‘𝑧)𝑉(2nd ‘𝑟)) |
60 | | breq 4585 |
. . . . . . . . . . 11
⊢ (◡𝑉 = 𝑉 → ((2nd ‘𝑟)◡𝑉(2nd ‘𝑧) ↔ (2nd ‘𝑟)𝑉(2nd ‘𝑧))) |
61 | 59, 60 | syl5rbbr 274 |
. . . . . . . . . 10
⊢ (◡𝑉 = 𝑉 → ((2nd ‘𝑟)𝑉(2nd ‘𝑧) ↔ (2nd ‘𝑧)𝑉(2nd ‘𝑟))) |
62 | 56, 61 | syl 17 |
. . . . . . . . 9
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → ((2nd ‘𝑟)𝑉(2nd ‘𝑧) ↔ (2nd ‘𝑧)𝑉(2nd ‘𝑟))) |
63 | 54, 62 | mpbird 246 |
. . . . . . . 8
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → (2nd ‘𝑟)𝑉(2nd ‘𝑧)) |
64 | | fvex 6113 |
. . . . . . . . . 10
⊢
(1st ‘𝑧) ∈ V |
65 | | fvex 6113 |
. . . . . . . . . 10
⊢
(1st ‘𝑟) ∈ V |
66 | | brcogw 5212 |
. . . . . . . . . . 11
⊢
((((1st ‘𝑧) ∈ V ∧ (2nd ‘𝑟) ∈ V ∧ (1st
‘𝑟) ∈ V) ∧
((1st ‘𝑧)𝑉(1st ‘𝑟) ∧ (1st ‘𝑟)𝑀(2nd ‘𝑟))) → (1st ‘𝑧)(𝑀 ∘ 𝑉)(2nd ‘𝑟)) |
67 | 66 | ex 449 |
. . . . . . . . . 10
⊢
(((1st ‘𝑧) ∈ V ∧ (2nd ‘𝑟) ∈ V ∧ (1st
‘𝑟) ∈ V) →
(((1st ‘𝑧)𝑉(1st ‘𝑟) ∧ (1st ‘𝑟)𝑀(2nd ‘𝑟)) → (1st ‘𝑧)(𝑀 ∘ 𝑉)(2nd ‘𝑟))) |
68 | 64, 57, 65, 67 | mp3an 1416 |
. . . . . . . . 9
⊢
(((1st ‘𝑧)𝑉(1st ‘𝑟) ∧ (1st ‘𝑟)𝑀(2nd ‘𝑟)) → (1st ‘𝑧)(𝑀 ∘ 𝑉)(2nd ‘𝑟)) |
69 | | brcogw 5212 |
. . . . . . . . . . 11
⊢
((((1st ‘𝑧) ∈ V ∧ (2nd ‘𝑧) ∈ V ∧ (2nd
‘𝑟) ∈ V) ∧
((1st ‘𝑧)(𝑀 ∘ 𝑉)(2nd ‘𝑟) ∧ (2nd ‘𝑟)𝑉(2nd ‘𝑧))) → (1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧)) |
70 | 69 | ex 449 |
. . . . . . . . . 10
⊢
(((1st ‘𝑧) ∈ V ∧ (2nd ‘𝑧) ∈ V ∧ (2nd
‘𝑟) ∈ V) →
(((1st ‘𝑧)(𝑀 ∘ 𝑉)(2nd ‘𝑟) ∧ (2nd ‘𝑟)𝑉(2nd ‘𝑧)) → (1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧))) |
71 | 64, 58, 57, 70 | mp3an 1416 |
. . . . . . . . 9
⊢
(((1st ‘𝑧)(𝑀 ∘ 𝑉)(2nd ‘𝑟) ∧ (2nd ‘𝑟)𝑉(2nd ‘𝑧)) → (1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧)) |
72 | 68, 71 | sylan 487 |
. . . . . . . 8
⊢
((((1st ‘𝑧)𝑉(1st ‘𝑟) ∧ (1st ‘𝑟)𝑀(2nd ‘𝑟)) ∧ (2nd ‘𝑟)𝑉(2nd ‘𝑧)) → (1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧)) |
73 | 41, 49, 63, 72 | syl21anc 1317 |
. . . . . . 7
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) ∧ 𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)) → (1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧)) |
74 | 73 | ralrimiva 2949 |
. . . . . 6
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → ∀𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)(1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧)) |
75 | | simplll 794 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑈 ∈ (UnifOn‘𝑋)) |
76 | | simplrl 796 |
. . . . . . . . 9
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑉 ∈ 𝑈) |
77 | 4 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑧 ∈ (𝑋 × 𝑋)) → 𝐽 ∈ Top) |
78 | | xp1st 7089 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑋 × 𝑋) → (1st ‘𝑧) ∈ 𝑋) |
79 | 2 | utopsnnei 21863 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ (1st ‘𝑧) ∈ 𝑋) → (𝑉 “ {(1st ‘𝑧)}) ∈ ((nei‘𝐽)‘{(1st
‘𝑧)})) |
80 | 78, 79 | syl3an3 1353 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑧 ∈ (𝑋 × 𝑋)) → (𝑉 “ {(1st ‘𝑧)}) ∈ ((nei‘𝐽)‘{(1st
‘𝑧)})) |
81 | | xp2nd 7090 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑋 × 𝑋) → (2nd ‘𝑧) ∈ 𝑋) |
82 | 2 | utopsnnei 21863 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ (2nd ‘𝑧) ∈ 𝑋) → (𝑉 “ {(2nd ‘𝑧)}) ∈ ((nei‘𝐽)‘{(2nd
‘𝑧)})) |
83 | 81, 82 | syl3an3 1353 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑧 ∈ (𝑋 × 𝑋)) → (𝑉 “ {(2nd ‘𝑧)}) ∈ ((nei‘𝐽)‘{(2nd
‘𝑧)})) |
84 | 14, 14 | neitx 21220 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ Top ∧ 𝐽 ∈ Top) ∧ ((𝑉 “ {(1st
‘𝑧)}) ∈
((nei‘𝐽)‘{(1st ‘𝑧)}) ∧ (𝑉 “ {(2nd ‘𝑧)}) ∈ ((nei‘𝐽)‘{(2nd
‘𝑧)}))) →
((𝑉 “
{(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘({(1st
‘𝑧)} ×
{(2nd ‘𝑧)}))) |
85 | 77, 77, 80, 83, 84 | syl22anc 1319 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑧 ∈ (𝑋 × 𝑋)) → ((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘({(1st
‘𝑧)} ×
{(2nd ‘𝑧)}))) |
86 | | 1st2nd2 7096 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (𝑋 × 𝑋) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
87 | 86 | sneqd 4137 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (𝑋 × 𝑋) → {𝑧} = {〈(1st ‘𝑧), (2nd ‘𝑧)〉}) |
88 | 64, 58 | xpsn 6313 |
. . . . . . . . . . . . 13
⊢
({(1st ‘𝑧)} × {(2nd ‘𝑧)}) = {〈(1st
‘𝑧), (2nd
‘𝑧)〉} |
89 | 87, 88 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ (𝑋 × 𝑋) → {𝑧} = ({(1st ‘𝑧)} × {(2nd
‘𝑧)})) |
90 | 89 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ (𝑋 × 𝑋) → ((nei‘(𝐽 ×t 𝐽))‘{𝑧}) = ((nei‘(𝐽 ×t 𝐽))‘({(1st ‘𝑧)} × {(2nd
‘𝑧)}))) |
91 | 90 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑧 ∈ (𝑋 × 𝑋)) → ((nei‘(𝐽 ×t 𝐽))‘{𝑧}) = ((nei‘(𝐽 ×t 𝐽))‘({(1st ‘𝑧)} × {(2nd
‘𝑧)}))) |
92 | 85, 91 | eleqtrrd 2691 |
. . . . . . . . 9
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑉 ∈ 𝑈 ∧ 𝑧 ∈ (𝑋 × 𝑋)) → ((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘{𝑧})) |
93 | 75, 76, 25, 92 | syl3anc 1318 |
. . . . . . . 8
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → ((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘{𝑧})) |
94 | 20 | neindisj 20731 |
. . . . . . . 8
⊢ ((((𝐽 ×t 𝐽) ∈ Top ∧ 𝑀 ⊆ ∪ (𝐽
×t 𝐽))
∧ (𝑧 ∈
((cls‘(𝐽
×t 𝐽))‘𝑀) ∧ ((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∈ ((nei‘(𝐽 ×t 𝐽))‘{𝑧}))) → (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀) ≠ ∅) |
95 | 7, 19, 24, 93, 94 | syl22anc 1319 |
. . . . . . 7
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀) ≠ ∅) |
96 | | r19.3rzv 4016 |
. . . . . . 7
⊢ ((((𝑉 “ {(1st
‘𝑧)}) × (𝑉 “ {(2nd
‘𝑧)})) ∩ 𝑀) ≠ ∅ →
((1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧) ↔ ∀𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)(1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧))) |
97 | 95, 96 | syl 17 |
. . . . . 6
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → ((1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧) ↔ ∀𝑟 ∈ (((𝑉 “ {(1st ‘𝑧)}) × (𝑉 “ {(2nd ‘𝑧)})) ∩ 𝑀)(1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧))) |
98 | 74, 97 | mpbird 246 |
. . . . 5
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → (1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧)) |
99 | | df-br 4584 |
. . . . 5
⊢
((1st ‘𝑧)(𝑉 ∘ (𝑀 ∘ 𝑉))(2nd ‘𝑧) ↔ 〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∈ (𝑉 ∘ (𝑀 ∘ 𝑉))) |
100 | 98, 99 | sylib 207 |
. . . 4
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∈ (𝑉 ∘ (𝑀 ∘ 𝑉))) |
101 | 27, 100 | eqeltrd 2688 |
. . 3
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) ∧ 𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀)) → 𝑧 ∈ (𝑉 ∘ (𝑀 ∘ 𝑉))) |
102 | 101 | ex 449 |
. 2
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) → (𝑧 ∈ ((cls‘(𝐽 ×t 𝐽))‘𝑀) → 𝑧 ∈ (𝑉 ∘ (𝑀 ∘ 𝑉)))) |
103 | 102 | ssrdv 3574 |
1
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑀 ⊆ (𝑋 × 𝑋)) ∧ (𝑉 ∈ 𝑈 ∧ ◡𝑉 = 𝑉)) → ((cls‘(𝐽 ×t 𝐽))‘𝑀) ⊆ (𝑉 ∘ (𝑀 ∘ 𝑉))) |