Metamath Proof Explorer

Theorem qtopval

Description: Value of the quotient topology function. (Contributed by Mario Carneiro, 23-Mar-2015)

Ref Expression
Hypothesis qtopval.1 ⊢ X = ⋃ J
Assertion qtopval ⊢ J ∈ V ∧ F ∈ W → J qTop F = s ∈ 𝒫 F X | F -1 s ∩ X ∈ J

Proof

Step Hyp Ref Expression
1 qtopval.1 ⊢ X = ⋃ J
2 elex ⊢ J ∈ V → J ∈ V
3 elex ⊢ F ∈ W → F ∈ V
4 imaexg ⊢ F ∈ V → F X ∈ V
5 pwexg ⊢ F X ∈ V → 𝒫 F X ∈ V
6 rabexg ⊢ 𝒫 F X ∈ V → s ∈ 𝒫 F X | F -1 s ∩ X ∈ J ∈ V
7 4 5 6 3syl ⊢ F ∈ V → s ∈ 𝒫 F X | F -1 s ∩ X ∈ J ∈ V
8 7 adantl ⊢ J ∈ V ∧ F ∈ V → s ∈ 𝒫 F X | F -1 s ∩ X ∈ J ∈ V
9 simpr ⊢ j = J ∧ f = F → f = F
10 simpl ⊢ j = J ∧ f = F → j = J
11 10 unieqd ⊢ j = J ∧ f = F → ⋃ j = ⋃ J
12 11 1 eqtr4di ⊢ j = J ∧ f = F → ⋃ j = X
13 9 12 imaeq12d ⊢ j = J ∧ f = F → f ⋃ j = F X
14 13 pweqd ⊢ j = J ∧ f = F → 𝒫 f ⋃ j = 𝒫 F X
15 9 cnveqd ⊢ j = J ∧ f = F → f -1 = F -1
16 15 imaeq1d ⊢ j = J ∧ f = F → f -1 s = F -1 s
17 16 12 ineq12d ⊢ j = J ∧ f = F → f -1 s ∩ ⋃ j = F -1 s ∩ X
18 17 10 eleq12d ⊢ j = J ∧ f = F → f -1 s ∩ ⋃ j ∈ j ↔ F -1 s ∩ X ∈ J
19 14 18 rabeqbidv ⊢ j = J ∧ f = F → s ∈ 𝒫 f ⋃ j | f -1 s ∩ ⋃ j ∈ j = s ∈ 𝒫 F X | F -1 s ∩ X ∈ J
20 df-qtop ⊢ qTop = j ∈ V , f ∈ V ⟼ s ∈ 𝒫 f ⋃ j | f -1 s ∩ ⋃ j ∈ j
21 19 20 ovmpoga ⊢ J ∈ V ∧ F ∈ V ∧ s ∈ 𝒫 F X | F -1 s ∩ X ∈ J ∈ V → J qTop F = s ∈ 𝒫 F X | F -1 s ∩ X ∈ J
22 8 21 mpd3an3 ⊢ J ∈ V ∧ F ∈ V → J qTop F = s ∈ 𝒫 F X | F -1 s ∩ X ∈ J
23 2 3 22 syl2an ⊢ J ∈ V ∧ F ∈ W → J qTop F = s ∈ 𝒫 F X | F -1 s ∩ X ∈ J