Step | Hyp | Ref
| Expression |
1 | | ucncn.5 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ ((UnifSt‘𝑅) Cnu(UnifSt‘𝑆))) |
2 | | ucncn.1 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ UnifSp) |
3 | | eqid 2740 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑅) |
4 | | eqid 2740 |
. . . . . . . 8
⊢
(UnifSt‘𝑅) =
(UnifSt‘𝑅) |
5 | | ucncn.j |
. . . . . . . 8
⊢ 𝐽 = (TopOpen‘𝑅) |
6 | 3, 4, 5 | isusp 23403 |
. . . . . . 7
⊢ (𝑅 ∈ UnifSp ↔
((UnifSt‘𝑅) ∈
(UnifOn‘(Base‘𝑅)) ∧ 𝐽 = (unifTop‘(UnifSt‘𝑅)))) |
7 | 6 | simplbi 498 |
. . . . . 6
⊢ (𝑅 ∈ UnifSp →
(UnifSt‘𝑅) ∈
(UnifOn‘(Base‘𝑅))) |
8 | 2, 7 | syl 17 |
. . . . 5
⊢ (𝜑 → (UnifSt‘𝑅) ∈
(UnifOn‘(Base‘𝑅))) |
9 | | ucncn.2 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ UnifSp) |
10 | | eqid 2740 |
. . . . . . . 8
⊢
(Base‘𝑆) =
(Base‘𝑆) |
11 | | eqid 2740 |
. . . . . . . 8
⊢
(UnifSt‘𝑆) =
(UnifSt‘𝑆) |
12 | | ucncn.k |
. . . . . . . 8
⊢ 𝐾 = (TopOpen‘𝑆) |
13 | 10, 11, 12 | isusp 23403 |
. . . . . . 7
⊢ (𝑆 ∈ UnifSp ↔
((UnifSt‘𝑆) ∈
(UnifOn‘(Base‘𝑆)) ∧ 𝐾 = (unifTop‘(UnifSt‘𝑆)))) |
14 | 13 | simplbi 498 |
. . . . . 6
⊢ (𝑆 ∈ UnifSp →
(UnifSt‘𝑆) ∈
(UnifOn‘(Base‘𝑆))) |
15 | 9, 14 | syl 17 |
. . . . 5
⊢ (𝜑 → (UnifSt‘𝑆) ∈
(UnifOn‘(Base‘𝑆))) |
16 | | isucn 23420 |
. . . . 5
⊢
(((UnifSt‘𝑅)
∈ (UnifOn‘(Base‘𝑅)) ∧ (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆))) → (𝐹 ∈ ((UnifSt‘𝑅) Cnu(UnifSt‘𝑆)) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))))) |
17 | 8, 15, 16 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (𝐹 ∈ ((UnifSt‘𝑅) Cnu(UnifSt‘𝑆)) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))))) |
18 | 1, 17 | mpbid 231 |
. . 3
⊢ (𝜑 → (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))) |
19 | 18 | simpld 495 |
. 2
⊢ (𝜑 → 𝐹:(Base‘𝑅)⟶(Base‘𝑆)) |
20 | | cnvimass 5987 |
. . . . 5
⊢ (◡𝐹 “ 𝑎) ⊆ dom 𝐹 |
21 | 19 | fdmd 6608 |
. . . . . 6
⊢ (𝜑 → dom 𝐹 = (Base‘𝑅)) |
22 | 21 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → dom 𝐹 = (Base‘𝑅)) |
23 | 20, 22 | sseqtrid 3978 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (◡𝐹 “ 𝑎) ⊆ (Base‘𝑅)) |
24 | | simplll 772 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝜑) |
25 | | simpr 485 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑠 ∈ (UnifSt‘𝑆)) |
26 | 23 | ad2antrr 723 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → (◡𝐹 “ 𝑎) ⊆ (Base‘𝑅)) |
27 | | simplr 766 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑥 ∈ (◡𝐹 “ 𝑎)) |
28 | 26, 27 | sseldd 3927 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑥 ∈ (Base‘𝑅)) |
29 | 18 | simprd 496 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
30 | 29 | r19.21bi 3135 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
31 | | r19.12 3255 |
. . . . . . . . . . 11
⊢
(∃𝑟 ∈
(UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → ∀𝑥 ∈ (Base‘𝑅)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
32 | 30, 31 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∀𝑥 ∈ (Base‘𝑅)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
33 | 32 | r19.21bi 3135 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
34 | 24, 25, 28, 33 | syl21anc 835 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
35 | 34 | adantr 481 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
36 | 24 | ad3antrrr 727 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → 𝜑) |
37 | 8 | ad5antr 731 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅))) |
38 | | simpr 485 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → 𝑟 ∈ (UnifSt‘𝑅)) |
39 | | ustrel 23353 |
. . . . . . . . . . . 12
⊢
(((UnifSt‘𝑅)
∈ (UnifOn‘(Base‘𝑅)) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑟) |
40 | 37, 38, 39 | syl2anc 584 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑟) |
41 | 40 | adantr 481 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → Rel 𝑟) |
42 | 36, 8 | syl 17 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅))) |
43 | | simplr 766 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → 𝑟 ∈ (UnifSt‘𝑅)) |
44 | 28 | ad3antrrr 727 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → 𝑥 ∈ (Base‘𝑅)) |
45 | | ustimasn 23370 |
. . . . . . . . . . 11
⊢
(((UnifSt‘𝑅)
∈ (UnifOn‘(Base‘𝑅)) ∧ 𝑟 ∈ (UnifSt‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) |
46 | 42, 43, 44, 45 | syl3anc 1370 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) |
47 | | simpr 485 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
48 | | simplr 766 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → 𝑧 ∈ (Base‘𝑅)) |
49 | | simpllr 773 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) |
50 | 15 | ad5antr 731 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆))) |
51 | | simpllr 773 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → 𝑠 ∈ (UnifSt‘𝑆)) |
52 | | ustrel 23353 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((UnifSt‘𝑆)
∈ (UnifOn‘(Base‘𝑆)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → Rel 𝑠) |
53 | 50, 51, 52 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑠) |
54 | | elrelimasn 5991 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Rel
𝑠 → ((𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)}) ↔ (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → ((𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)}) ↔ (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
56 | 55 | biimpar 478 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)})) |
57 | 49, 56 | sseldd 3927 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ 𝑎) |
58 | 57 | adantlr 712 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ 𝑎) |
59 | | ffn 6597 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) → 𝐹 Fn (Base‘𝑅)) |
60 | | elpreima 6930 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 Fn (Base‘𝑅) → (𝑧 ∈ (◡𝐹 “ 𝑎) ↔ (𝑧 ∈ (Base‘𝑅) ∧ (𝐹‘𝑧) ∈ 𝑎))) |
61 | 19, 59, 60 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑧 ∈ (◡𝐹 “ 𝑎) ↔ (𝑧 ∈ (Base‘𝑅) ∧ (𝐹‘𝑧) ∈ 𝑎))) |
62 | 61 | ad7antr 735 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝑧 ∈ (◡𝐹 “ 𝑎) ↔ (𝑧 ∈ (Base‘𝑅) ∧ (𝐹‘𝑧) ∈ 𝑎))) |
63 | 48, 58, 62 | mpbir2and 710 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → 𝑧 ∈ (◡𝐹 “ 𝑎)) |
64 | 63 | ex 413 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) → ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
65 | 64 | ralrimiva 3110 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
66 | 65 | adantr 481 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
67 | | r19.26 3097 |
. . . . . . . . . . . 12
⊢
(∀𝑧 ∈
(Base‘𝑅)((𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎))) ↔ (∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎)))) |
68 | | pm3.33 762 |
. . . . . . . . . . . . 13
⊢ (((𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎))) → (𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
69 | 68 | ralimi 3089 |
. . . . . . . . . . . 12
⊢
(∀𝑧 ∈
(Base‘𝑅)((𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
70 | 67, 69 | sylbir 234 |
. . . . . . . . . . 11
⊢
((∀𝑧 ∈
(Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
71 | 47, 66, 70 | syl2anc 584 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
72 | | simpl2l 1225 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → Rel 𝑟) |
73 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (𝑟 “ {𝑥})) |
74 | | elrelimasn 5991 |
. . . . . . . . . . . . . . 15
⊢ (Rel
𝑟 → (𝑦 ∈ (𝑟 “ {𝑥}) ↔ 𝑥𝑟𝑦)) |
75 | 74 | biimpa 477 |
. . . . . . . . . . . . . 14
⊢ ((Rel
𝑟 ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑥𝑟𝑦) |
76 | 72, 73, 75 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑥𝑟𝑦) |
77 | | breq2 5083 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑦 → (𝑥𝑟𝑧 ↔ 𝑥𝑟𝑦)) |
78 | | eleq1w 2823 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑦 → (𝑧 ∈ (◡𝐹 “ 𝑎) ↔ 𝑦 ∈ (◡𝐹 “ 𝑎))) |
79 | 77, 78 | imbi12d 345 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑦 → ((𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎)) ↔ (𝑥𝑟𝑦 → 𝑦 ∈ (◡𝐹 “ 𝑎)))) |
80 | | simpl3 1192 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
81 | | simpl2r 1226 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) |
82 | 81, 73 | sseldd 3927 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (Base‘𝑅)) |
83 | 79, 80, 82 | rspcdva 3563 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → (𝑥𝑟𝑦 → 𝑦 ∈ (◡𝐹 “ 𝑎))) |
84 | 76, 83 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (◡𝐹 “ 𝑎)) |
85 | 84 | ex 413 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) → (𝑦 ∈ (𝑟 “ {𝑥}) → 𝑦 ∈ (◡𝐹 “ 𝑎))) |
86 | 85 | ssrdv 3932 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) → (𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)) |
87 | 36, 41, 46, 71, 86 | syl121anc 1374 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → (𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)) |
88 | 87 | ex 413 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎))) |
89 | 88 | reximdva 3205 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) → (∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎))) |
90 | 35, 89 | mpd 15 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)) |
91 | | sneq 4577 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑥) → {𝑦} = {(𝐹‘𝑥)}) |
92 | 91 | imaeq2d 5967 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑥) → (𝑠 “ {𝑦}) = (𝑠 “ {(𝐹‘𝑥)})) |
93 | 92 | sseq1d 3957 |
. . . . . . . 8
⊢ (𝑦 = (𝐹‘𝑥) → ((𝑠 “ {𝑦}) ⊆ 𝑎 ↔ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎)) |
94 | 93 | rexbidv 3228 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝑥) → (∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎 ↔ ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎)) |
95 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝑎 ∈ 𝐾) |
96 | 13 | simprbi 497 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ UnifSp → 𝐾 =
(unifTop‘(UnifSt‘𝑆))) |
97 | 9, 96 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 = (unifTop‘(UnifSt‘𝑆))) |
98 | 97 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝐾 = (unifTop‘(UnifSt‘𝑆))) |
99 | 95, 98 | eleqtrd 2843 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝑎 ∈ (unifTop‘(UnifSt‘𝑆))) |
100 | | elutop 23375 |
. . . . . . . . . . . 12
⊢
((UnifSt‘𝑆)
∈ (UnifOn‘(Base‘𝑆)) → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎))) |
101 | 15, 100 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎))) |
102 | 101 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎))) |
103 | 99, 102 | mpbid 231 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)) |
104 | 103 | simprd 496 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎) |
105 | 104 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) → ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎) |
106 | | elpreima 6930 |
. . . . . . . . . . 11
⊢ (𝐹 Fn (Base‘𝑅) → (𝑥 ∈ (◡𝐹 “ 𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎))) |
107 | 19, 59, 106 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (◡𝐹 “ 𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎))) |
108 | 107 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (𝑥 ∈ (◡𝐹 “ 𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎))) |
109 | 108 | biimpa 477 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) → (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎)) |
110 | 109 | simprd 496 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) → (𝐹‘𝑥) ∈ 𝑎) |
111 | 94, 105, 110 | rspcdva 3563 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) → ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) |
112 | 90, 111 | r19.29a 3220 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)) |
113 | 112 | ralrimiva 3110 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ∀𝑥 ∈ (◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)) |
114 | 6 | simprbi 497 |
. . . . . . . 8
⊢ (𝑅 ∈ UnifSp → 𝐽 =
(unifTop‘(UnifSt‘𝑅))) |
115 | 2, 114 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐽 = (unifTop‘(UnifSt‘𝑅))) |
116 | 115 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝐽 = (unifTop‘(UnifSt‘𝑅))) |
117 | 116 | eleq2d 2826 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ((◡𝐹 “ 𝑎) ∈ 𝐽 ↔ (◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)))) |
118 | | elutop 23375 |
. . . . . . 7
⊢
((UnifSt‘𝑅)
∈ (UnifOn‘(Base‘𝑅)) → ((◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)))) |
119 | 8, 118 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)))) |
120 | 119 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ((◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)))) |
121 | 117, 120 | bitrd 278 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ((◡𝐹 “ 𝑎) ∈ 𝐽 ↔ ((◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)))) |
122 | 23, 113, 121 | mpbir2and 710 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (◡𝐹 “ 𝑎) ∈ 𝐽) |
123 | 122 | ralrimiva 3110 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ 𝐾 (◡𝐹 “ 𝑎) ∈ 𝐽) |
124 | | ucncn.3 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ TopSp) |
125 | 3, 5 | istps 22073 |
. . . 4
⊢ (𝑅 ∈ TopSp ↔ 𝐽 ∈
(TopOn‘(Base‘𝑅))) |
126 | 124, 125 | sylib 217 |
. . 3
⊢ (𝜑 → 𝐽 ∈ (TopOn‘(Base‘𝑅))) |
127 | | ucncn.4 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ TopSp) |
128 | 10, 12 | istps 22073 |
. . . 4
⊢ (𝑆 ∈ TopSp ↔ 𝐾 ∈
(TopOn‘(Base‘𝑆))) |
129 | 127, 128 | sylib 217 |
. . 3
⊢ (𝜑 → 𝐾 ∈ (TopOn‘(Base‘𝑆))) |
130 | | iscn 22376 |
. . 3
⊢ ((𝐽 ∈
(TopOn‘(Base‘𝑅)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝑆))) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑎 ∈ 𝐾 (◡𝐹 “ 𝑎) ∈ 𝐽))) |
131 | 126, 129,
130 | syl2anc 584 |
. 2
⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑎 ∈ 𝐾 (◡𝐹 “ 𝑎) ∈ 𝐽))) |
132 | 19, 123, 131 | mpbir2and 710 |
1
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |