Step | Hyp | Ref
| Expression |
1 | | utopval 22413 |
. . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑎}) |
2 | | ssrab2 3914 |
. . . 4
⊢ {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑎} ⊆ 𝒫 𝑋 |
3 | 1, 2 | syl6eqss 3880 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ⊆ 𝒫 𝑋) |
4 | | ssidd 3849 |
. . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 ⊆ 𝑋) |
5 | | ustssxp 22385 |
. . . . . . . . 9
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑣 ∈ 𝑈) → 𝑣 ⊆ (𝑋 × 𝑋)) |
6 | | imassrn 5722 |
. . . . . . . . . 10
⊢ (𝑣 “ {𝑥}) ⊆ ran 𝑣 |
7 | | rnss 5590 |
. . . . . . . . . . 11
⊢ (𝑣 ⊆ (𝑋 × 𝑋) → ran 𝑣 ⊆ ran (𝑋 × 𝑋)) |
8 | | rnxpid 5812 |
. . . . . . . . . . 11
⊢ ran
(𝑋 × 𝑋) = 𝑋 |
9 | 7, 8 | syl6sseq 3876 |
. . . . . . . . . 10
⊢ (𝑣 ⊆ (𝑋 × 𝑋) → ran 𝑣 ⊆ 𝑋) |
10 | 6, 9 | syl5ss 3838 |
. . . . . . . . 9
⊢ (𝑣 ⊆ (𝑋 × 𝑋) → (𝑣 “ {𝑥}) ⊆ 𝑋) |
11 | 5, 10 | syl 17 |
. . . . . . . 8
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑣 ∈ 𝑈) → (𝑣 “ {𝑥}) ⊆ 𝑋) |
12 | 11 | ralrimiva 3175 |
. . . . . . 7
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∀𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋) |
13 | | ustne0 22394 |
. . . . . . . 8
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 ≠ ∅) |
14 | | r19.2zb 4285 |
. . . . . . . 8
⊢ (𝑈 ≠ ∅ ↔
(∀𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋 → ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋)) |
15 | 13, 14 | sylib 210 |
. . . . . . 7
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (∀𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋 → ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋)) |
16 | 12, 15 | mpd 15 |
. . . . . 6
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋) |
17 | 16 | ralrimivw 3176 |
. . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋) |
18 | | elutop 22414 |
. . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 ∈ (unifTop‘𝑈) ↔ (𝑋 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋))) |
19 | 4, 17, 18 | mpbir2and 704 |
. . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 ∈ (unifTop‘𝑈)) |
20 | | elpwuni 4839 |
. . . 4
⊢ (𝑋 ∈ (unifTop‘𝑈) → ((unifTop‘𝑈) ⊆ 𝒫 𝑋 ↔ ∪ (unifTop‘𝑈) = 𝑋)) |
21 | 19, 20 | syl 17 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ((unifTop‘𝑈) ⊆ 𝒫 𝑋 ↔ ∪ (unifTop‘𝑈) = 𝑋)) |
22 | 3, 21 | mpbid 224 |
. 2
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ (unifTop‘𝑈) = 𝑋) |
23 | 22 | eqcomd 2831 |
1
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = ∪
(unifTop‘𝑈)) |