Metamath Proof Explorer

Theorem elqtop

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

Ref Expression
Hypothesis qtopval.1 ⊢ X = ⋃ J
Assertion elqtop ⊢ J ∈ V ∧ F : Z ⟶ onto Y ∧ Z ⊆ X → A ∈ J qTop F ↔ A ⊆ Y ∧ F -1 A ∈ J

Proof

Step Hyp Ref Expression
1 qtopval.1 ⊢ X = ⋃ J
2 1 qtopval2 ⊢ J ∈ V ∧ F : Z ⟶ onto Y ∧ Z ⊆ X → J qTop F = s ∈ 𝒫 Y | F -1 s ∈ J
3 2 eleq2d ⊢ J ∈ V ∧ F : Z ⟶ onto Y ∧ Z ⊆ X → A ∈ J qTop F ↔ A ∈ s ∈ 𝒫 Y | F -1 s ∈ J
4 imaeq2 ⊢ s = A → F -1 s = F -1 A
5 4 eleq1d ⊢ s = A → F -1 s ∈ J ↔ F -1 A ∈ J
6 5 elrab ⊢ A ∈ s ∈ 𝒫 Y | F -1 s ∈ J ↔ A ∈ 𝒫 Y ∧ F -1 A ∈ J
7 uniexg ⊢ J ∈ V → ⋃ J ∈ V
8 1 7 eqeltrid ⊢ J ∈ V → X ∈ V
9 8 3ad2ant1 ⊢ J ∈ V ∧ F : Z ⟶ onto Y ∧ Z ⊆ X → X ∈ V
10 simp3 ⊢ J ∈ V ∧ F : Z ⟶ onto Y ∧ Z ⊆ X → Z ⊆ X
11 9 10 ssexd ⊢ J ∈ V ∧ F : Z ⟶ onto Y ∧ Z ⊆ X → Z ∈ V
12 simp2 ⊢ J ∈ V ∧ F : Z ⟶ onto Y ∧ Z ⊆ X → F : Z ⟶ onto Y
13 focdmex ⊢ Z ∈ V → F : Z ⟶ onto Y → Y ∈ V
14 11 12 13 sylc ⊢ J ∈ V ∧ F : Z ⟶ onto Y ∧ Z ⊆ X → Y ∈ V
15 elpw2g ⊢ Y ∈ V → A ∈ 𝒫 Y ↔ A ⊆ Y
16 14 15 syl ⊢ J ∈ V ∧ F : Z ⟶ onto Y ∧ Z ⊆ X → A ∈ 𝒫 Y ↔ A ⊆ Y
17 16 anbi1d ⊢ J ∈ V ∧ F : Z ⟶ onto Y ∧ Z ⊆ X → A ∈ 𝒫 Y ∧ F -1 A ∈ J ↔ A ⊆ Y ∧ F -1 A ∈ J
18 6 17 bitrid ⊢ J ∈ V ∧ F : Z ⟶ onto Y ∧ Z ⊆ X → A ∈ s ∈ 𝒫 Y | F -1 s ∈ J ↔ A ⊆ Y ∧ F -1 A ∈ J
19 3 18 bitrd ⊢ J ∈ V ∧ F : Z ⟶ onto Y ∧ Z ⊆ X → A ∈ J qTop F ↔ A ⊆ Y ∧ F -1 A ∈ J