| Step | Hyp | Ref
| Expression |
| 1 | | ucncn.5 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ ((UnifSt‘𝑅) Cnu(UnifSt‘𝑆))) |
| 2 | | ucncn.1 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ UnifSp) |
| 3 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 4 | | eqid 2737 |
. . . . . . . 8
⊢
(UnifSt‘𝑅) =
(UnifSt‘𝑅) |
| 5 | | ucncn.j |
. . . . . . . 8
⊢ 𝐽 = (TopOpen‘𝑅) |
| 6 | 3, 4, 5 | isusp 24270 |
. . . . . . 7
⊢ (𝑅 ∈ UnifSp ↔
((UnifSt‘𝑅) ∈
(UnifOn‘(Base‘𝑅)) ∧ 𝐽 = (unifTop‘(UnifSt‘𝑅)))) |
| 7 | 6 | simplbi 497 |
. . . . . 6
⊢ (𝑅 ∈ UnifSp →
(UnifSt‘𝑅) ∈
(UnifOn‘(Base‘𝑅))) |
| 8 | 2, 7 | syl 17 |
. . . . 5
⊢ (𝜑 → (UnifSt‘𝑅) ∈
(UnifOn‘(Base‘𝑅))) |
| 9 | | ucncn.2 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ UnifSp) |
| 10 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝑆) =
(Base‘𝑆) |
| 11 | | eqid 2737 |
. . . . . . . 8
⊢
(UnifSt‘𝑆) =
(UnifSt‘𝑆) |
| 12 | | ucncn.k |
. . . . . . . 8
⊢ 𝐾 = (TopOpen‘𝑆) |
| 13 | 10, 11, 12 | isusp 24270 |
. . . . . . 7
⊢ (𝑆 ∈ UnifSp ↔
((UnifSt‘𝑆) ∈
(UnifOn‘(Base‘𝑆)) ∧ 𝐾 = (unifTop‘(UnifSt‘𝑆)))) |
| 14 | 13 | simplbi 497 |
. . . . . 6
⊢ (𝑆 ∈ UnifSp →
(UnifSt‘𝑆) ∈
(UnifOn‘(Base‘𝑆))) |
| 15 | 9, 14 | syl 17 |
. . . . 5
⊢ (𝜑 → (UnifSt‘𝑆) ∈
(UnifOn‘(Base‘𝑆))) |
| 16 | | isucn 24287 |
. . . . 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 232 |
. . 3
⊢ (𝜑 → (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)))) |
| 19 | 18 | simpld 494 |
. 2
⊢ (𝜑 → 𝐹:(Base‘𝑅)⟶(Base‘𝑆)) |
| 20 | | cnvimass 6100 |
. . . . 5
⊢ (◡𝐹 “ 𝑎) ⊆ dom 𝐹 |
| 21 | 19 | fdmd 6746 |
. . . . . 6
⊢ (𝜑 → dom 𝐹 = (Base‘𝑅)) |
| 22 | 21 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → dom 𝐹 = (Base‘𝑅)) |
| 23 | 20, 22 | sseqtrid 4026 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (◡𝐹 “ 𝑎) ⊆ (Base‘𝑅)) |
| 24 | | simplll 775 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝜑) |
| 25 | | simpr 484 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑠 ∈ (UnifSt‘𝑆)) |
| 26 | 23 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → (◡𝐹 “ 𝑎) ⊆ (Base‘𝑅)) |
| 27 | | simplr 769 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑥 ∈ (◡𝐹 “ 𝑎)) |
| 28 | 26, 27 | sseldd 3984 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → 𝑥 ∈ (Base‘𝑅)) |
| 29 | 18 | simprd 495 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑠 ∈ (UnifSt‘𝑆)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
| 30 | 29 | r19.21bi 3251 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
| 31 | | r19.12 3314 |
. . . . . . . . . . 11
⊢
(∃𝑟 ∈
(UnifSt‘𝑅)∀𝑥 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → ∀𝑥 ∈ (Base‘𝑅)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
| 32 | 30, 31 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∀𝑥 ∈ (Base‘𝑅)∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
| 33 | 32 | r19.21bi 3251 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ 𝑥 ∈ (Base‘𝑅)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
| 34 | 24, 25, 28, 33 | syl21anc 838 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
| 35 | 34 | adantr 480 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) → ∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
| 36 | 24 | ad3antrrr 730 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → 𝜑) |
| 37 | 8 | ad5antr 734 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅))) |
| 38 | | simpr 484 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → 𝑟 ∈ (UnifSt‘𝑅)) |
| 39 | | ustrel 24220 |
. . . . . . . . . . . 12
⊢
(((UnifSt‘𝑅)
∈ (UnifOn‘(Base‘𝑅)) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑟) |
| 40 | 37, 38, 39 | syl2anc 584 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑟) |
| 41 | 40 | adantr 480 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → Rel 𝑟) |
| 42 | 36, 8 | syl 17 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → (UnifSt‘𝑅) ∈ (UnifOn‘(Base‘𝑅))) |
| 43 | | simplr 769 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → 𝑟 ∈ (UnifSt‘𝑅)) |
| 44 | 28 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → 𝑥 ∈ (Base‘𝑅)) |
| 45 | | ustimasn 24237 |
. . . . . . . . . . 11
⊢
(((UnifSt‘𝑅)
∈ (UnifOn‘(Base‘𝑅)) ∧ 𝑟 ∈ (UnifSt‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) |
| 46 | 42, 43, 44, 45 | syl3anc 1373 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) |
| 47 | | simpr 484 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
| 48 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → 𝑧 ∈ (Base‘𝑅)) |
| 49 | | simpllr 776 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) |
| 50 | 15 | ad5antr 734 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (UnifSt‘𝑆) ∈ (UnifOn‘(Base‘𝑆))) |
| 51 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → 𝑠 ∈ (UnifSt‘𝑆)) |
| 52 | | ustrel 24220 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((UnifSt‘𝑆)
∈ (UnifOn‘(Base‘𝑆)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) → Rel 𝑠) |
| 53 | 50, 51, 52 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → Rel 𝑠) |
| 54 | | elrelimasn 6104 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Rel
𝑠 → ((𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)}) ↔ (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
| 55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → ((𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)}) ↔ (𝐹‘𝑥)𝑠(𝐹‘𝑧))) |
| 56 | 55 | biimpar 477 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ (𝑠 “ {(𝐹‘𝑥)})) |
| 57 | 49, 56 | sseldd 3984 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ 𝑎) |
| 58 | 57 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝐹‘𝑧) ∈ 𝑎) |
| 59 | | ffn 6736 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) → 𝐹 Fn (Base‘𝑅)) |
| 60 | | elpreima 7078 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹 Fn (Base‘𝑅) → (𝑧 ∈ (◡𝐹 “ 𝑎) ↔ (𝑧 ∈ (Base‘𝑅) ∧ (𝐹‘𝑧) ∈ 𝑎))) |
| 61 | 19, 59, 60 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑧 ∈ (◡𝐹 “ 𝑎) ↔ (𝑧 ∈ (Base‘𝑅) ∧ (𝐹‘𝑧) ∈ 𝑎))) |
| 62 | 61 | ad7antr 738 |
. . . . . . . . . . . . . . 15
⊢
((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝑧 ∈ (◡𝐹 “ 𝑎) ↔ (𝑧 ∈ (Base‘𝑅) ∧ (𝐹‘𝑧) ∈ 𝑎))) |
| 63 | 48, 58, 62 | mpbir2and 713 |
. . . . . . . . . . . . . 14
⊢
((((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) ∧ (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → 𝑧 ∈ (◡𝐹 “ 𝑎)) |
| 64 | 63 | ex 412 |
. . . . . . . . . . . . 13
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ 𝑧 ∈ (Base‘𝑅)) → ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
| 65 | 64 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
| 66 | 65 | adantr 480 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
| 67 | | r19.26 3111 |
. . . . . . . . . . . 12
⊢
(∀𝑧 ∈
(Base‘𝑅)((𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎))) ↔ (∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎)))) |
| 68 | | pm3.33 765 |
. . . . . . . . . . . . 13
⊢ (((𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎))) → (𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
| 69 | 68 | ralimi 3083 |
. . . . . . . . . . . 12
⊢
(∀𝑧 ∈
(Base‘𝑅)((𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
| 70 | 67, 69 | sylbir 235 |
. . . . . . . . . . 11
⊢
((∀𝑧 ∈
(Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) ∧ ∀𝑧 ∈ (Base‘𝑅)((𝐹‘𝑥)𝑠(𝐹‘𝑧) → 𝑧 ∈ (◡𝐹 “ 𝑎))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
| 71 | 47, 66, 70 | syl2anc 584 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
| 72 | | simpl2l 1227 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → Rel 𝑟) |
| 73 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (𝑟 “ {𝑥})) |
| 74 | | elrelimasn 6104 |
. . . . . . . . . . . . . . 15
⊢ (Rel
𝑟 → (𝑦 ∈ (𝑟 “ {𝑥}) ↔ 𝑥𝑟𝑦)) |
| 75 | 74 | biimpa 476 |
. . . . . . . . . . . . . 14
⊢ ((Rel
𝑟 ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑥𝑟𝑦) |
| 76 | 72, 73, 75 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑥𝑟𝑦) |
| 77 | | breq2 5147 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑦 → (𝑥𝑟𝑧 ↔ 𝑥𝑟𝑦)) |
| 78 | | eleq1w 2824 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑦 → (𝑧 ∈ (◡𝐹 “ 𝑎) ↔ 𝑦 ∈ (◡𝐹 “ 𝑎))) |
| 79 | 77, 78 | imbi12d 344 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑦 → ((𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎)) ↔ (𝑥𝑟𝑦 → 𝑦 ∈ (◡𝐹 “ 𝑎)))) |
| 80 | | simpl3 1194 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) |
| 81 | | simpl2r 1228 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) |
| 82 | 81, 73 | sseldd 3984 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (Base‘𝑅)) |
| 83 | 79, 80, 82 | rspcdva 3623 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → (𝑥𝑟𝑦 → 𝑦 ∈ (◡𝐹 “ 𝑎))) |
| 84 | 76, 83 | mpd 15 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) ∧ 𝑦 ∈ (𝑟 “ {𝑥})) → 𝑦 ∈ (◡𝐹 “ 𝑎)) |
| 85 | 84 | ex 412 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) → (𝑦 ∈ (𝑟 “ {𝑥}) → 𝑦 ∈ (◡𝐹 “ 𝑎))) |
| 86 | 85 | ssrdv 3989 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (Rel 𝑟 ∧ (𝑟 “ {𝑥}) ⊆ (Base‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → 𝑧 ∈ (◡𝐹 “ 𝑎))) → (𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)) |
| 87 | 36, 41, 46, 71, 86 | syl121anc 1377 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) ∧ ∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧))) → (𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)) |
| 88 | 87 | ex 412 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) ∧ 𝑟 ∈ (UnifSt‘𝑅)) → (∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → (𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎))) |
| 89 | 88 | reximdva 3168 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) → (∃𝑟 ∈ (UnifSt‘𝑅)∀𝑧 ∈ (Base‘𝑅)(𝑥𝑟𝑧 → (𝐹‘𝑥)𝑠(𝐹‘𝑧)) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎))) |
| 90 | 35, 89 | mpd 15 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) ∧ 𝑠 ∈ (UnifSt‘𝑆)) ∧ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)) |
| 91 | | sneq 4636 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑥) → {𝑦} = {(𝐹‘𝑥)}) |
| 92 | 91 | imaeq2d 6078 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑥) → (𝑠 “ {𝑦}) = (𝑠 “ {(𝐹‘𝑥)})) |
| 93 | 92 | sseq1d 4015 |
. . . . . . . 8
⊢ (𝑦 = (𝐹‘𝑥) → ((𝑠 “ {𝑦}) ⊆ 𝑎 ↔ (𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎)) |
| 94 | 93 | rexbidv 3179 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝑥) → (∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎 ↔ ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎)) |
| 95 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝑎 ∈ 𝐾) |
| 96 | 13 | simprbi 496 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ UnifSp → 𝐾 =
(unifTop‘(UnifSt‘𝑆))) |
| 97 | 9, 96 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 = (unifTop‘(UnifSt‘𝑆))) |
| 98 | 97 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝐾 = (unifTop‘(UnifSt‘𝑆))) |
| 99 | 95, 98 | eleqtrd 2843 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝑎 ∈ (unifTop‘(UnifSt‘𝑆))) |
| 100 | | elutop 24242 |
. . . . . . . . . . . 12
⊢
((UnifSt‘𝑆)
∈ (UnifOn‘(Base‘𝑆)) → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎))) |
| 101 | 15, 100 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎))) |
| 102 | 101 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (𝑎 ∈ (unifTop‘(UnifSt‘𝑆)) ↔ (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎))) |
| 103 | 99, 102 | mpbid 232 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (𝑎 ⊆ (Base‘𝑆) ∧ ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎)) |
| 104 | 103 | simprd 495 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎) |
| 105 | 104 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) → ∀𝑦 ∈ 𝑎 ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {𝑦}) ⊆ 𝑎) |
| 106 | | elpreima 7078 |
. . . . . . . . . . 11
⊢ (𝐹 Fn (Base‘𝑅) → (𝑥 ∈ (◡𝐹 “ 𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎))) |
| 107 | 19, 59, 106 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (◡𝐹 “ 𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎))) |
| 108 | 107 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (𝑥 ∈ (◡𝐹 “ 𝑎) ↔ (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎))) |
| 109 | 108 | biimpa 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) → (𝑥 ∈ (Base‘𝑅) ∧ (𝐹‘𝑥) ∈ 𝑎)) |
| 110 | 109 | simprd 495 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) → (𝐹‘𝑥) ∈ 𝑎) |
| 111 | 94, 105, 110 | rspcdva 3623 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) → ∃𝑠 ∈ (UnifSt‘𝑆)(𝑠 “ {(𝐹‘𝑥)}) ⊆ 𝑎) |
| 112 | 90, 111 | r19.29a 3162 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐾) ∧ 𝑥 ∈ (◡𝐹 “ 𝑎)) → ∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)) |
| 113 | 112 | ralrimiva 3146 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ∀𝑥 ∈ (◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)) |
| 114 | 6 | simprbi 496 |
. . . . . . . 8
⊢ (𝑅 ∈ UnifSp → 𝐽 =
(unifTop‘(UnifSt‘𝑅))) |
| 115 | 2, 114 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐽 = (unifTop‘(UnifSt‘𝑅))) |
| 116 | 115 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → 𝐽 = (unifTop‘(UnifSt‘𝑅))) |
| 117 | 116 | eleq2d 2827 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ((◡𝐹 “ 𝑎) ∈ 𝐽 ↔ (◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)))) |
| 118 | | elutop 24242 |
. . . . . . 7
⊢
((UnifSt‘𝑅)
∈ (UnifOn‘(Base‘𝑅)) → ((◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)))) |
| 119 | 8, 118 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)))) |
| 120 | 119 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ((◡𝐹 “ 𝑎) ∈ (unifTop‘(UnifSt‘𝑅)) ↔ ((◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)))) |
| 121 | 117, 120 | bitrd 279 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → ((◡𝐹 “ 𝑎) ∈ 𝐽 ↔ ((◡𝐹 “ 𝑎) ⊆ (Base‘𝑅) ∧ ∀𝑥 ∈ (◡𝐹 “ 𝑎)∃𝑟 ∈ (UnifSt‘𝑅)(𝑟 “ {𝑥}) ⊆ (◡𝐹 “ 𝑎)))) |
| 122 | 23, 113, 121 | mpbir2and 713 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐾) → (◡𝐹 “ 𝑎) ∈ 𝐽) |
| 123 | 122 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ 𝐾 (◡𝐹 “ 𝑎) ∈ 𝐽) |
| 124 | | ucncn.3 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ TopSp) |
| 125 | 3, 5 | istps 22940 |
. . . 4
⊢ (𝑅 ∈ TopSp ↔ 𝐽 ∈
(TopOn‘(Base‘𝑅))) |
| 126 | 124, 125 | sylib 218 |
. . 3
⊢ (𝜑 → 𝐽 ∈ (TopOn‘(Base‘𝑅))) |
| 127 | | ucncn.4 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ TopSp) |
| 128 | 10, 12 | istps 22940 |
. . . 4
⊢ (𝑆 ∈ TopSp ↔ 𝐾 ∈
(TopOn‘(Base‘𝑆))) |
| 129 | 127, 128 | sylib 218 |
. . 3
⊢ (𝜑 → 𝐾 ∈ (TopOn‘(Base‘𝑆))) |
| 130 | | iscn 23243 |
. . 3
⊢ ((𝐽 ∈
(TopOn‘(Base‘𝑅)) ∧ 𝐾 ∈ (TopOn‘(Base‘𝑆))) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑎 ∈ 𝐾 (◡𝐹 “ 𝑎) ∈ 𝐽))) |
| 131 | 126, 129,
130 | syl2anc 584 |
. 2
⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:(Base‘𝑅)⟶(Base‘𝑆) ∧ ∀𝑎 ∈ 𝐾 (◡𝐹 “ 𝑎) ∈ 𝐽))) |
| 132 | 19, 123, 131 | mpbir2and 713 |
1
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |