| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | utoptop.1 | . . . . . . . 8
⊢ 𝐽 = (unifTop‘𝑈) | 
| 2 |  | utopval 24241 | . . . . . . . 8
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎}) | 
| 3 | 1, 2 | eqtrid 2789 | . . . . . . 7
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎}) | 
| 4 |  | simpll 767 | . . . . . . . . . . 11
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → 𝑈 ∈ (UnifOn‘𝑋)) | 
| 5 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑎 ∈ 𝒫 𝑋) | 
| 6 | 5 | elpwid 4609 | . . . . . . . . . . . 12
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → 𝑎 ⊆ 𝑋) | 
| 7 | 6 | sselda 3983 | . . . . . . . . . . 11
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → 𝑝 ∈ 𝑋) | 
| 8 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → 𝑝 ∈ 𝑋) | 
| 9 |  | mptexg 7241 | . . . . . . . . . . . . . . . 16
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V) | 
| 10 |  | rnexg 7924 | . . . . . . . . . . . . . . . 16
⊢ ((𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V) | 
| 11 | 9, 10 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V) | 
| 12 | 11 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V) | 
| 13 |  | utopsnneip.2 | . . . . . . . . . . . . . . 15
⊢ 𝑁 = (𝑝 ∈ 𝑋 ↦ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) | 
| 14 | 13 | fvmpt2 7027 | . . . . . . . . . . . . . 14
⊢ ((𝑝 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ∈ V) → (𝑁‘𝑝) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) | 
| 15 | 8, 12, 14 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑁‘𝑝) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝}))) | 
| 16 | 15 | eleq2d 2827 | . . . . . . . . . . . 12
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑎 ∈ (𝑁‘𝑝) ↔ 𝑎 ∈ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})))) | 
| 17 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢ (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) = (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) | 
| 18 | 17 | elrnmpt 5969 | . . . . . . . . . . . . 13
⊢ (𝑎 ∈ V → (𝑎 ∈ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}))) | 
| 19 | 18 | elv 3485 | . . . . . . . . . . . 12
⊢ (𝑎 ∈ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) | 
| 20 | 16, 19 | bitrdi 287 | . . . . . . . . . . 11
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}))) | 
| 21 | 4, 7, 20 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}))) | 
| 22 |  | nfv 1914 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑣((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) | 
| 23 |  | nfre1 3285 | . . . . . . . . . . . . 13
⊢
Ⅎ𝑣∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}) | 
| 24 | 22, 23 | nfan 1899 | . . . . . . . . . . . 12
⊢
Ⅎ𝑣(((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) | 
| 25 |  | simplr 769 | . . . . . . . . . . . . 13
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) ∧ 𝑣 ∈ 𝑈) ∧ 𝑎 = (𝑣 “ {𝑝})) → 𝑣 ∈ 𝑈) | 
| 26 |  | eqimss2 4043 | . . . . . . . . . . . . . 14
⊢ (𝑎 = (𝑣 “ {𝑝}) → (𝑣 “ {𝑝}) ⊆ 𝑎) | 
| 27 | 26 | adantl 481 | . . . . . . . . . . . . 13
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) ∧ 𝑣 ∈ 𝑈) ∧ 𝑎 = (𝑣 “ {𝑝})) → (𝑣 “ {𝑝}) ⊆ 𝑎) | 
| 28 |  | imaeq1 6073 | . . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑣 → (𝑤 “ {𝑝}) = (𝑣 “ {𝑝})) | 
| 29 | 28 | sseq1d 4015 | . . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑣 → ((𝑤 “ {𝑝}) ⊆ 𝑎 ↔ (𝑣 “ {𝑝}) ⊆ 𝑎)) | 
| 30 | 29 | rspcev 3622 | . . . . . . . . . . . . 13
⊢ ((𝑣 ∈ 𝑈 ∧ (𝑣 “ {𝑝}) ⊆ 𝑎) → ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎) | 
| 31 | 25, 27, 30 | syl2anc 584 | . . . . . . . . . . . 12
⊢
((((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) ∧ 𝑣 ∈ 𝑈) ∧ 𝑎 = (𝑣 “ {𝑝})) → ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎) | 
| 32 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) → ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) | 
| 33 | 24, 31, 32 | r19.29af 3268 | . . . . . . . . . . 11
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) → ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎) | 
| 34 | 4 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑈 ∈ (UnifOn‘𝑋)) | 
| 35 | 7 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑝 ∈ 𝑋) | 
| 36 | 34, 35 | jca 511 | . . . . . . . . . . . . . 14
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → (𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋)) | 
| 37 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → (𝑤 “ {𝑝}) ⊆ 𝑎) | 
| 38 | 6 | ad3antrrr 730 | . . . . . . . . . . . . . 14
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑎 ⊆ 𝑋) | 
| 39 |  | simplr 769 | . . . . . . . . . . . . . . 15
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑤 ∈ 𝑈) | 
| 40 |  | eqid 2737 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑤 “ {𝑝}) = (𝑤 “ {𝑝}) | 
| 41 |  | imaeq1 6073 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 𝑤 → (𝑢 “ {𝑝}) = (𝑤 “ {𝑝})) | 
| 42 | 41 | rspceeqv 3645 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∈ 𝑈 ∧ (𝑤 “ {𝑝}) = (𝑤 “ {𝑝})) → ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝})) | 
| 43 | 40, 42 | mpan2 691 | . . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ 𝑈 → ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝})) | 
| 44 | 43 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝})) | 
| 45 |  | vex 3484 | . . . . . . . . . . . . . . . . . . 19
⊢ 𝑤 ∈ V | 
| 46 | 45 | imaex 7936 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑤 “ {𝑝}) ∈ V | 
| 47 | 13 | ustuqtoplem 24248 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ∈ V) → ((𝑤 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))) | 
| 48 | 46, 47 | mpan2 691 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → ((𝑤 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))) | 
| 49 | 48 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → ((𝑤 “ {𝑝}) ∈ (𝑁‘𝑝) ↔ ∃𝑢 ∈ 𝑈 (𝑤 “ {𝑝}) = (𝑢 “ {𝑝}))) | 
| 50 | 44, 49 | mpbird 257 | . . . . . . . . . . . . . . 15
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑤 ∈ 𝑈) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝)) | 
| 51 | 34, 35, 39, 50 | syl21anc 838 | . . . . . . . . . . . . . 14
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝)) | 
| 52 |  | sseq1 4009 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ⊆ 𝑎 ↔ (𝑤 “ {𝑝}) ⊆ 𝑎)) | 
| 53 | 52 | 3anbi2d 1443 | . . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑤 “ {𝑝}) → (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑏 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ↔ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋))) | 
| 54 |  | eleq1 2829 | . . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑤 “ {𝑝}) → (𝑏 ∈ (𝑁‘𝑝) ↔ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝))) | 
| 55 | 53, 54 | anbi12d 632 | . . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑤 “ {𝑝}) → ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑏 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑝)) ↔ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝)))) | 
| 56 | 55 | imbi1d 341 | . . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑤 “ {𝑝}) → (((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑏 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑝)) → 𝑎 ∈ (𝑁‘𝑝)) ↔ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝)) → 𝑎 ∈ (𝑁‘𝑝)))) | 
| 57 | 13 | ustuqtop1 24250 | . . . . . . . . . . . . . . 15
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑏 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ 𝑏 ∈ (𝑁‘𝑝)) → 𝑎 ∈ (𝑁‘𝑝)) | 
| 58 | 46, 56, 57 | vtocl 3558 | . . . . . . . . . . . . . 14
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎 ∧ 𝑎 ⊆ 𝑋) ∧ (𝑤 “ {𝑝}) ∈ (𝑁‘𝑝)) → 𝑎 ∈ (𝑁‘𝑝)) | 
| 59 | 36, 37, 38, 51, 58 | syl31anc 1375 | . . . . . . . . . . . . 13
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → 𝑎 ∈ (𝑁‘𝑝)) | 
| 60 | 36, 20 | syl 17 | . . . . . . . . . . . . 13
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}))) | 
| 61 | 59, 60 | mpbid 232 | . . . . . . . . . . . 12
⊢
(((((𝑈 ∈
(UnifOn‘𝑋) ∧
𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ 𝑤 ∈ 𝑈) ∧ (𝑤 “ {𝑝}) ⊆ 𝑎) → ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) | 
| 62 | 61 | r19.29an 3158 | . . . . . . . . . . 11
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) ∧ ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎) → ∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝})) | 
| 63 | 33, 62 | impbida 801 | . . . . . . . . . 10
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → (∃𝑣 ∈ 𝑈 𝑎 = (𝑣 “ {𝑝}) ↔ ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎)) | 
| 64 | 21, 63 | bitrd 279 | . . . . . . . . 9
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) ∧ 𝑝 ∈ 𝑎) → (𝑎 ∈ (𝑁‘𝑝) ↔ ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎)) | 
| 65 | 64 | ralbidva 3176 | . . . . . . . 8
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑎 ∈ 𝒫 𝑋) → (∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝) ↔ ∀𝑝 ∈ 𝑎 ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎)) | 
| 66 | 65 | rabbidva 3443 | . . . . . . 7
⊢ (𝑈 ∈ (UnifOn‘𝑋) → {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 ∃𝑤 ∈ 𝑈 (𝑤 “ {𝑝}) ⊆ 𝑎}) | 
| 67 | 3, 66 | eqtr4d 2780 | . . . . . 6
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)}) | 
| 68 |  | utopsnneip.1 | . . . . . 6
⊢ 𝐾 = {𝑎 ∈ 𝒫 𝑋 ∣ ∀𝑝 ∈ 𝑎 𝑎 ∈ (𝑁‘𝑝)} | 
| 69 | 67, 68 | eqtr4di 2795 | . . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐽 = 𝐾) | 
| 70 | 69 | fveq2d 6910 | . . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (nei‘𝐽) = (nei‘𝐾)) | 
| 71 | 70 | fveq1d 6908 | . . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ((nei‘𝐽)‘{𝑃}) = ((nei‘𝐾)‘{𝑃})) | 
| 72 | 71 | adantr 480 | . 2
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐽)‘{𝑃}) = ((nei‘𝐾)‘{𝑃})) | 
| 73 | 13 | ustuqtop0 24249 | . . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑁:𝑋⟶𝒫 𝒫 𝑋) | 
| 74 | 13 | ustuqtop1 24250 | . . . . 5
⊢ ((((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑏 ∈ (𝑁‘𝑝)) | 
| 75 | 13 | ustuqtop2 24251 | . . . . 5
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → (fi‘(𝑁‘𝑝)) ⊆ (𝑁‘𝑝)) | 
| 76 | 13 | ustuqtop3 24252 | . . . . 5
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → 𝑝 ∈ 𝑎) | 
| 77 | 13 | ustuqtop4 24253 | . . . . 5
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) ∧ 𝑎 ∈ (𝑁‘𝑝)) → ∃𝑏 ∈ (𝑁‘𝑝)∀𝑞 ∈ 𝑏 𝑎 ∈ (𝑁‘𝑞)) | 
| 78 | 13 | ustuqtop5 24254 | . . . . 5
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑝 ∈ 𝑋) → 𝑋 ∈ (𝑁‘𝑝)) | 
| 79 | 68, 73, 74, 75, 76, 77, 78 | neiptopnei 23140 | . . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐾)‘{𝑝}))) | 
| 80 | 79 | adantr 480 | . . 3
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → 𝑁 = (𝑝 ∈ 𝑋 ↦ ((nei‘𝐾)‘{𝑝}))) | 
| 81 |  | simpr 484 | . . . . 5
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑝 = 𝑃) → 𝑝 = 𝑃) | 
| 82 | 81 | sneqd 4638 | . . . 4
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑝 = 𝑃) → {𝑝} = {𝑃}) | 
| 83 | 82 | fveq2d 6910 | . . 3
⊢ (((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) ∧ 𝑝 = 𝑃) → ((nei‘𝐾)‘{𝑝}) = ((nei‘𝐾)‘{𝑃})) | 
| 84 |  | simpr 484 | . . 3
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → 𝑃 ∈ 𝑋) | 
| 85 |  | fvexd 6921 | . . 3
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐾)‘{𝑃}) ∈ V) | 
| 86 | 80, 83, 84, 85 | fvmptd 7023 | . 2
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑁‘𝑃) = ((nei‘𝐾)‘{𝑃})) | 
| 87 |  | mptexg 7241 | . . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) | 
| 88 |  | rnexg 7924 | . . . . 5
⊢ ((𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) | 
| 89 | 87, 88 | syl 17 | . . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) | 
| 90 | 89 | adantr 480 | . . 3
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) | 
| 91 |  | nfv 1914 | . . . . . . . 8
⊢
Ⅎ𝑣 𝑃 ∈ 𝑋 | 
| 92 |  | nfmpt1 5250 | . . . . . . . . . 10
⊢
Ⅎ𝑣(𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) | 
| 93 | 92 | nfrn 5963 | . . . . . . . . 9
⊢
Ⅎ𝑣ran
(𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) | 
| 94 | 93 | nfel1 2922 | . . . . . . . 8
⊢
Ⅎ𝑣ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V | 
| 95 | 91, 94 | nfan 1899 | . . . . . . 7
⊢
Ⅎ𝑣(𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) | 
| 96 |  | nfv 1914 | . . . . . . 7
⊢
Ⅎ𝑣 𝑝 = 𝑃 | 
| 97 | 95, 96 | nfan 1899 | . . . . . 6
⊢
Ⅎ𝑣((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) ∧ 𝑝 = 𝑃) | 
| 98 |  | simpr2 1196 | . . . . . . . . 9
⊢ ((𝑃 ∈ 𝑋 ∧ (ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V ∧ 𝑝 = 𝑃 ∧ 𝑣 ∈ 𝑈)) → 𝑝 = 𝑃) | 
| 99 | 98 | sneqd 4638 | . . . . . . . 8
⊢ ((𝑃 ∈ 𝑋 ∧ (ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V ∧ 𝑝 = 𝑃 ∧ 𝑣 ∈ 𝑈)) → {𝑝} = {𝑃}) | 
| 100 | 99 | imaeq2d 6078 | . . . . . . 7
⊢ ((𝑃 ∈ 𝑋 ∧ (ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V ∧ 𝑝 = 𝑃 ∧ 𝑣 ∈ 𝑈)) → (𝑣 “ {𝑝}) = (𝑣 “ {𝑃})) | 
| 101 | 100 | 3anassrs 1361 | . . . . . 6
⊢ ((((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) ∧ 𝑝 = 𝑃) ∧ 𝑣 ∈ 𝑈) → (𝑣 “ {𝑝}) = (𝑣 “ {𝑃})) | 
| 102 | 97, 101 | mpteq2da 5240 | . . . . 5
⊢ (((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) ∧ 𝑝 = 𝑃) → (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) = (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃}))) | 
| 103 | 102 | rneqd 5949 | . . . 4
⊢ (((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) ∧ 𝑝 = 𝑃) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑝})) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃}))) | 
| 104 |  | simpl 482 | . . . 4
⊢ ((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) → 𝑃 ∈ 𝑋) | 
| 105 |  | simpr 484 | . . . 4
⊢ ((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) → ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) | 
| 106 | 13, 103, 104, 105 | fvmptd2 7024 | . . 3
⊢ ((𝑃 ∈ 𝑋 ∧ ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃})) ∈ V) → (𝑁‘𝑃) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃}))) | 
| 107 | 84, 90, 106 | syl2anc 584 | . 2
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → (𝑁‘𝑃) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃}))) | 
| 108 | 72, 86, 107 | 3eqtr2d 2783 | 1
⊢ ((𝑈 ∈ (UnifOn‘𝑋) ∧ 𝑃 ∈ 𝑋) → ((nei‘𝐽)‘{𝑃}) = ran (𝑣 ∈ 𝑈 ↦ (𝑣 “ {𝑃}))) |