Step | Hyp | Ref
| Expression |
1 | | ucncn.5 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ ((UnifSt‘𝑅) Cnu(UnifSt‘𝑆))) |
2 | | ucncn.1 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ UnifSp) |
3 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑅) |
4 | | eqid 2622 |
. . . . . . . 8
⊢
(UnifSt‘𝑅) =
(UnifSt‘𝑅) |
5 | | ucncn.j |
. . . . . . . 8
⊢ 𝐽 = (TopOpen‘𝑅) |
6 | 3, 4, 5 | isusp 22065 |
. . . . . . 7
⊢ (𝑅 ∈ UnifSp ↔
((UnifSt‘𝑅) ∈
(UnifOn‘(Base‘𝑅)) ∧ 𝐽 = (unifTop‘(UnifSt‘𝑅)))) |
7 | 6 | simplbi 476 |
. . . . . 6
⊢ (𝑅 ∈ UnifSp →
(UnifSt‘𝑅) ∈
(UnifOn‘(Base‘𝑅))) |
8 | 2, 7 | syl 17 |
. . . . 5
⊢ (𝜑 → (UnifSt‘𝑅) ∈
(UnifOn‘(Base‘𝑅))) |
9 | | ucncn.2 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ UnifSp) |
10 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘𝑆) =
(Base‘𝑆) |
11 | | eqid 2622 |
. . . . . . . 8
⊢
(UnifSt‘𝑆) =
(UnifSt‘𝑆) |
12 | | ucncn.k |
. . . . . . . 8
⊢ 𝐾 = (TopOpen‘𝑆) |
13 | 10, 11, 12 | isusp 22065 |
. . . . . . 7
⊢ (𝑆 ∈ UnifSp ↔
((UnifSt‘𝑆) ∈
(UnifOn‘(Base‘𝑆)) ∧ 𝐾 = (unifTop‘(UnifSt‘𝑆)))) |
14 | 13 | simplbi 476 |
. . . . . 6
⊢ (𝑆 ∈ UnifSp →
(UnifSt‘𝑆) ∈
(UnifOn‘(Base‘𝑆))) |
15 | 9, 14 | syl 17 |
. . . . 5
⊢ (𝜑 → (UnifSt‘𝑆) ∈
(UnifOn‘(Base‘𝑆))) |
16 | | isucn 22082 |
. . . . 5
⊢
(((UnifSt‘𝑅)
∈ (UnifOn‘(Base‘𝑅)) ∧ (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆))) → (𝐹 ∈ ((UnifSt‘𝑅) Cnu(UnifSt‘𝑆)) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))))) |
17 | 8, 15, 16 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (𝐹 ∈ ((UnifSt‘𝑅) Cnu(UnifSt‘𝑆)) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))))) |
18 | 1, 17 | mpbid 222 |
. . 3
⊢ (𝜑 → (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))) |
19 | 18 | simpld 475 |
. 2
⊢ (𝜑 → 𝐹:(Base‘𝑅)⟶(Base‘𝑆)) |
20 | | cnvimass 5485 |
. . . . 5
⊢ (◡𝐹 “ 𝑎) ⊆ dom 𝐹 |
21 | | fdm 6051 |
. . . . . . 7
⊢ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) → dom 𝐹 = (Base‘𝑅)) |
22 | 19, 21 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom 𝐹 = (Base‘𝑅)) |
23 | 22 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → dom 𝐹 = (Base‘𝑅)) |
24 | 20, 23 | syl5sseq 3653 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (◡𝐹 “ 𝑎) ⊆ (Base‘𝑅)) |
25 | | simplll 798 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝜑) |
26 | | simpr 477 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑠 ∈ (UnifSt‘𝑆)) |
27 | 24 | ad2antrr 762 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → (◡𝐹 “ 𝑎) ⊆ (Base‘𝑅)) |
28 | | simplr 792 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑥 ∈ (◡𝐹 “ 𝑎)) |
29 | 27, 28 | sseldd 3604 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑥 ∈ (Base‘𝑅)) |
30 | 18 | simprd 479 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
31 | 30 | r19.21bi 2932 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
32 | | r19.12 3063 |
. . . . . . . . . . 11
⊢
(∃𝑟 ∈
(UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → ∀𝑥 ∈ (Base‘𝑅)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
33 | 31, 32 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∀𝑥 ∈ (Base‘𝑅)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
34 | 33 | r19.21bi 2932 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
35 | 25, 26, 29, 34 | syl21anc 1325 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
36 | 35 | adantr 481 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
37 | 25 | ad3antrrr 766 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → 𝜑) |
38 | 8 | ad5antr 770 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅))) |
39 | | simpr 477 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → 𝑟 ∈ (UnifSt‘𝑅)) |
40 | | ustrel 22015 |
. . . . . . . . . . . 12
⊢
(((UnifSt‘𝑅)
∈ (UnifOn‘(Base‘𝑅)) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑟) |
41 | 38, 39, 40 | syl2anc 693 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑟) |
42 | 41 | adantr 481 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → Rel 𝑟) |
43 | 37, 8 | syl 17 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅))) |
44 | | simplr 792 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → 𝑟 ∈ (UnifSt‘𝑅)) |
45 | 29 | ad3antrrr 766 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → 𝑥 ∈ (Base‘𝑅)) |
46 | | ustimasn 22032 |
. . . . . . . . . . 11
⊢
(((UnifSt‘𝑅)
∈ (UnifOn‘(Base‘𝑅)) ∧ 𝑟 ∈ (UnifSt‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) |
47 | 43, 44, 45, 46 | syl3anc 1326 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) |
48 | | simpr 477 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
49 | | simplr 792 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → 𝑧 ∈ (Base‘𝑅)) |
50 | | simpllr 799 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) |
51 | 15 | ad5antr 770 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆))) |
52 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → 𝑠 ∈ (UnifSt‘𝑆)) |
53 | | ustrel 22015 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((UnifSt‘𝑆)
∈ (UnifOn‘(Base‘𝑆)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → Rel 𝑠) |
54 | 51, 52, 53 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑠) |
55 | | elrelimasn 5489 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Rel
𝑠 → ((𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)}) ↔ (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → ((𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)}) ↔ (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
57 | 56 | biimpar 502 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)})) |
58 | 50, 57 | sseldd 3604 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ 𝑎) |
59 | 58 | adantlr 751 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ 𝑎) |
60 | | ffn 6045 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) → 𝐹 Fn (Base‘𝑅)) |
61 | | elpreima 6337 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 Fn (Base‘𝑅) → (𝑧 ∈ (◡𝐹 “ 𝑎) ↔ (𝑧 ∈ (Base‘𝑅) ∧ (𝐹‘𝑧) ∈ 𝑎))) |
62 | 19, 60, 61 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑧 ∈ (◡𝐹 “ 𝑎) ↔ (𝑧 ∈ (Base‘𝑅) ∧ (𝐹‘𝑧) ∈ 𝑎))) |
63 | 62 | ad7antr 774 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝑧 ∈ (◡𝐹 “ 𝑎) ↔ (𝑧 ∈ (Base‘𝑅) ∧ (𝐹‘𝑧) ∈ 𝑎))) |
64 | 49, 59, 63 | mpbir2and 957 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → 𝑧 ∈ (◡𝐹 “ 𝑎)) |
65 | 64 | ex 450 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) → ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
66 | 65 | ralrimiva 2966 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
67 | 66 | adantr 481 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
68 | | r19.26 3064 |
. . . . . . . . . . . 12
⊢
(∀𝑧 ∈
(Base‘𝑅)((𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎))) ↔ (∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎)))) |
69 | | pm3.33 609 |
. . . . . . . . . . . . 13
⊢ (((𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎))) → (𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
70 | 69 | ralimi 2952 |
. . . . . . . . . . . 12
⊢
(∀𝑧 ∈
(Base‘𝑅)((𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
71 | 68, 70 | sylbir 225 |
. . . . . . . . . . 11
⊢
((∀𝑧 ∈
(Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
72 | 48, 67, 71 | syl2anc 693 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
73 | | simpl2l 1114 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → Rel 𝑟) |
74 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (𝑟 “ {𝑥})) |
75 | | elrelimasn 5489 |
. . . . . . . . . . . . . . 15
⊢ (Rel
𝑟 → (𝑦 ∈ (𝑟 “ {𝑥}) ↔ 𝑥𝑟𝑦)) |
76 | 75 | biimpa 501 |
. . . . . . . . . . . . . 14
⊢ ((Rel
𝑟 ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑥𝑟𝑦) |
77 | 73, 74, 76 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑥𝑟𝑦) |
78 | | simpl2r 1115 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) |
79 | 78, 74 | sseldd 3604 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (Base‘𝑅)) |
80 | | simpl3 1066 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
81 | | breq2 4657 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑦 → (𝑥𝑟𝑧 ↔ 𝑥𝑟𝑦)) |
82 | | eleq1 2689 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑦 → (𝑧 ∈ (◡𝐹 “ 𝑎) ↔ 𝑦 ∈ (◡𝐹 “ 𝑎))) |
83 | 81, 82 | imbi12d 334 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑦 → ((𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎)) ↔ (𝑥𝑟𝑦 → 𝑦 ∈ (◡𝐹 “ 𝑎)))) |
84 | 83 | rspcv 3305 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (Base‘𝑅) → (∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎)) → (𝑥𝑟𝑦 → 𝑦 ∈ (◡𝐹 “ 𝑎)))) |
85 | 79, 80, 84 | sylc 65 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → (𝑥𝑟𝑦 → 𝑦 ∈ (◡𝐹 “ 𝑎))) |
86 | 77, 85 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (◡𝐹 “ 𝑎)) |
87 | 86 | ex 450 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) → (𝑦 ∈ (𝑟 “ {𝑥}) → 𝑦 ∈ (◡𝐹 “ 𝑎))) |
88 | 87 | ssrdv 3609 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) → (𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)) |
89 | 37, 42, 47, 72, 88 | syl121anc 1331 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → (𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)) |
90 | 89 | ex 450 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎))) |
91 | 90 | reximdva 3017 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) → (∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎))) |
92 | 36, 91 | mpd 15 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)) |
93 | | elpreima 6337 |
. . . . . . . . . . 11
⊢ (𝐹 Fn (Base‘𝑅) → (𝑥 ∈ (◡𝐹 “ 𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎))) |
94 | 19, 60, 93 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (◡𝐹 “ 𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎))) |
95 | 94 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (𝑥 ∈ (◡𝐹 “ 𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎))) |
96 | 95 | biimpa 501 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) → (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎)) |
97 | 96 | simprd 479 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) → (𝐹‘𝑥) ∈ 𝑎) |
98 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝑎 ∈ 𝐾) |
99 | 13 | simprbi 480 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ UnifSp → 𝐾 =
(unifTop‘(UnifSt‘𝑆))) |
100 | 9, 99 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 = (unifTop‘(UnifSt‘𝑆))) |
101 | 100 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝐾 = (unifTop‘(UnifSt‘𝑆))) |
102 | 98, 101 | eleqtrd 2703 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝑎 ∈ (unifTop‘(UnifSt‘𝑆))) |
103 | | elutop 22037 |
. . . . . . . . . . . 12
⊢
((UnifSt‘𝑆)
∈ (UnifOn‘(Base‘𝑆)) → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎))) |
104 | 15, 103 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎))) |
105 | 104 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎))) |
106 | 102, 105 | mpbid 222 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)) |
107 | 106 | simprd 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎) |
108 | 107 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) → ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎) |
109 | | sneq 4187 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐹‘𝑥) → {𝑦} = {(𝐹‘𝑥)}) |
110 | 109 | imaeq2d 5466 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑥) → (𝑠 “ {𝑦}) = (𝑠 “ {(𝐹‘𝑥)})) |
111 | 110 | sseq1d 3632 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑥) → ((𝑠 “ {𝑦}) ⊆ 𝑎 ↔ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎)) |
112 | 111 | rexbidv 3052 |
. . . . . . . 8
⊢ (𝑦 = (𝐹‘𝑥) → (∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎 ↔ ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎)) |
113 | 112 | rspcv 3305 |
. . . . . . 7
⊢ ((𝐹‘𝑥) ∈ 𝑎 → (∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎 → ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎)) |
114 | 97, 108, 113 | sylc 65 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) → ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) |
115 | 92, 114 | r19.29a 3078 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)) |
116 | 115 | ralrimiva 2966 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ∀𝑥 ∈ (◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)) |
117 | 6 | simprbi 480 |
. . . . . . . 8
⊢ (𝑅 ∈ UnifSp → 𝐽 =
(unifTop‘(UnifSt‘𝑅))) |
118 | 2, 117 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐽 = (unifTop‘(UnifSt‘𝑅))) |
119 | 118 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝐽 = (unifTop‘(UnifSt‘𝑅))) |
120 | 119 | eleq2d 2687 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ((◡𝐹 “ 𝑎) ∈ 𝐽 ↔ (◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)))) |
121 | | elutop 22037 |
. . . . . . 7
⊢
((UnifSt‘𝑅)
∈ (UnifOn‘(Base‘𝑅)) → ((◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)))) |
122 | 8, 121 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)))) |
123 | 122 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ((◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)))) |
124 | 120, 123 | bitrd 268 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ((◡𝐹 “ 𝑎) ∈ 𝐽 ↔ ((◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)))) |
125 | 24, 116, 124 | mpbir2and 957 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (◡𝐹 “ 𝑎) ∈ 𝐽) |
126 | 125 | ralrimiva 2966 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ 𝐾 (◡𝐹 “ 𝑎) ∈ 𝐽) |
127 | | ucncn.3 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ TopSp) |
128 | 3, 5 | istps 20738 |
. . . 4
⊢ (𝑅 ∈ TopSp ↔ 𝐽 ∈
(TopOn‘(Base‘𝑅))) |
129 | 127, 128 | sylib 208 |
. . 3
⊢ (𝜑 → 𝐽 ∈ (TopOn‘(Base‘𝑅))) |
130 | | ucncn.4 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ TopSp) |
131 | 10, 12 | istps 20738 |
. . . 4
⊢ (𝑆 ∈ TopSp ↔ 𝐾 ∈
(TopOn‘(Base‘𝑆))) |
132 | 130, 131 | sylib 208 |
. . 3
⊢ (𝜑 → 𝐾 ∈ (TopOn‘(Base‘𝑆))) |
133 | | iscn 21039 |
. . 3
⊢ ((𝐽 ∈
(TopOn‘(Base‘𝑅)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝑆))) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑎 ∈ 𝐾 (◡𝐹 “ 𝑎) ∈ 𝐽))) |
134 | 129, 132,
133 | syl2anc 693 |
. 2
⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑎 ∈ 𝐾 (◡𝐹 “ 𝑎) ∈ 𝐽))) |
135 | 19, 126, 134 | mpbir2and 957 |
1
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |