| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | utopval 24242 | . . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑎}) | 
| 2 |  | ssrab2 4079 | . . . 4
⊢ {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑥 ∈ 𝑎 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑎} ⊆ 𝒫 𝑋 | 
| 3 | 1, 2 | eqsstrdi 4027 | . . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) ⊆ 𝒫 𝑋) | 
| 4 |  | ssidd 4006 | . . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 ⊆ 𝑋) | 
| 5 |  | ustssxp 24214 | . . . . . . . . 9
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑣 ∈ 𝑈) → 𝑣 ⊆ (𝑋 × 𝑋)) | 
| 6 |  | imassrn 6088 | . . . . . . . . . 10
⊢ (𝑣 “ {𝑥}) ⊆ ran 𝑣 | 
| 7 |  | rnss 5949 | . . . . . . . . . . 11
⊢ (𝑣 ⊆ (𝑋 × 𝑋) → ran 𝑣 ⊆ ran (𝑋 × 𝑋)) | 
| 8 |  | rnxpid 6192 | . . . . . . . . . . 11
⊢ ran
(𝑋 × 𝑋) = 𝑋 | 
| 9 | 7, 8 | sseqtrdi 4023 | . . . . . . . . . 10
⊢ (𝑣 ⊆ (𝑋 × 𝑋) → ran 𝑣 ⊆ 𝑋) | 
| 10 | 6, 9 | sstrid 3994 | . . . . . . . . 9
⊢ (𝑣 ⊆ (𝑋 × 𝑋) → (𝑣 “ {𝑥}) ⊆ 𝑋) | 
| 11 | 5, 10 | syl 17 | . . . . . . . 8
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑣 ∈ 𝑈) → (𝑣 “ {𝑥}) ⊆ 𝑋) | 
| 12 | 11 | ralrimiva 3145 | . . . . . . 7
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∀𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋) | 
| 13 |  | ustne0 24223 | . . . . . . . 8
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 ≠ ∅) | 
| 14 |  | r19.2zb 4495 | . . . . . . . 8
⊢ (𝑈 ≠ ∅ ↔
(∀𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋 → ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋)) | 
| 15 | 13, 14 | sylib 218 | . . . . . . 7
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (∀𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋 → ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋)) | 
| 16 | 12, 15 | mpd 15 | . . . . . 6
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋) | 
| 17 | 16 | ralrimivw 3149 | . . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋) | 
| 18 |  | elutop 24243 | . . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 ∈ (unifTop‘𝑈) ↔ (𝑋 ⊆ 𝑋 ∧ ∀𝑥 ∈ 𝑋 ∃𝑣 ∈ 𝑈 (𝑣 “ {𝑥}) ⊆ 𝑋))) | 
| 19 | 4, 17, 18 | mpbir2and 713 | . . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 ∈ (unifTop‘𝑈)) | 
| 20 |  | elpwuni 5104 | . . . 4
⊢ (𝑋 ∈ (unifTop‘𝑈) → ((unifTop‘𝑈) ⊆ 𝒫 𝑋 ↔ ∪ (unifTop‘𝑈) = 𝑋)) | 
| 21 | 19, 20 | syl 17 | . . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ((unifTop‘𝑈) ⊆ 𝒫 𝑋 ↔ ∪ (unifTop‘𝑈) = 𝑋)) | 
| 22 | 3, 21 | mpbid 232 | . 2
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ (unifTop‘𝑈) = 𝑋) | 
| 23 | 22 | eqcomd 2742 | 1
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = ∪
(unifTop‘𝑈)) |