Step | Hyp | Ref
| Expression |
1 | | utopval 22036 |
. . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑎}) |
2 | | ssrab2 3687 |
. . . 4
⊢ {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑎} ⊆ 𝒫 𝑋 |
3 | 1, 2 | syl6eqss 3655 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ⊆ 𝒫 𝑋) |
4 | | ssid 3624 |
. . . . . 6
⊢ 𝑋 ⊆ 𝑋 |
5 | 4 | a1i 11 |
. . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 ⊆ 𝑋) |
6 | | ustssxp 22008 |
. . . . . . . . 9
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑣 ∈ 𝑈) → 𝑣 ⊆ (𝑋 × 𝑋)) |
7 | | imassrn 5477 |
. . . . . . . . . 10
⊢ (𝑣 “ {𝑥}) ⊆ ran 𝑣 |
8 | | rnss 5354 |
. . . . . . . . . . 11
⊢ (𝑣 ⊆ (𝑋 × 𝑋) → ran 𝑣 ⊆ ran (𝑋 × 𝑋)) |
9 | | rnxpid 5567 |
. . . . . . . . . . 11
⊢ ran
(𝑋 × 𝑋) = 𝑋 |
10 | 8, 9 | syl6sseq 3651 |
. . . . . . . . . 10
⊢ (𝑣 ⊆ (𝑋 × 𝑋) → ran 𝑣 ⊆ 𝑋) |
11 | 7, 10 | syl5ss 3614 |
. . . . . . . . 9
⊢ (𝑣 ⊆ (𝑋 × 𝑋) → (𝑣 “ {𝑥}) ⊆ 𝑋) |
12 | 6, 11 | syl 17 |
. . . . . . . 8
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑣 ∈ 𝑈) → (𝑣 “ {𝑥}) ⊆ 𝑋) |
13 | 12 | ralrimiva 2966 |
. . . . . . 7
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∀𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋) |
14 | | ustne0 22017 |
. . . . . . . 8
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 ≠ ∅) |
15 | | r19.2zb 4061 |
. . . . . . . 8
⊢ (𝑈 ≠ ∅ ↔
(∀𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋 → ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋)) |
16 | 14, 15 | sylib 208 |
. . . . . . 7
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (∀𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋 → ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋)) |
17 | 13, 16 | mpd 15 |
. . . . . 6
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋) |
18 | 17 | ralrimivw 2967 |
. . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋) |
19 | | elutop 22037 |
. . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 ∈ (unifTop‘𝑈) ↔ (𝑋 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋))) |
20 | 5, 18, 19 | mpbir2and 957 |
. . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 ∈ (unifTop‘𝑈)) |
21 | | elpwuni 4616 |
. . . 4
⊢ (𝑋 ∈ (unifTop‘𝑈) → ((unifTop‘𝑈) ⊆ 𝒫 𝑋 ↔ ∪ (unifTop‘𝑈) = 𝑋)) |
22 | 20, 21 | syl 17 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ((unifTop‘𝑈) ⊆ 𝒫 𝑋 ↔ ∪ (unifTop‘𝑈) = 𝑋)) |
23 | 3, 22 | mpbid 222 |
. 2
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ (unifTop‘𝑈) = 𝑋) |
24 | 23 | eqcomd 2628 |
1
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = ∪
(unifTop‘𝑈)) |