qtopval2

Description: Value of the quotient topology function when F is a function on the base set. (Contributed by Mario Carneiro, 23-Mar-2015)

		Ref	Expression
	Hypothesis	qtopval.1	$⊢ X = ⋃ J$
	Assertion	qtopval2	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to J qTop F = \{s \in 𝒫 Y \| F^{-1} [s] \in J\}$

Proof

Step	Hyp	Ref	Expression
1		qtopval.1	$⊢ X = ⋃ J$
2		simp1	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to J \in V$
3		fof	$⊢ F : Z \underset{onto}{⟶} Y \to F : Z ⟶ Y$
4	3	3ad2ant2	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to F : Z ⟶ Y$
5		uniexg	$⊢ J \in V \to ⋃ J \in V$
6	5	3ad2ant1	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to ⋃ J \in V$
7	1 6	eqeltrid	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to X \in V$
8		simp3	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to Z \subseteq X$
9	7 8	ssexd	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to Z \in V$
10		fex	$⊢ (F : Z ⟶ Y \land Z \in V) \to F \in V$
11	4 9 10	syl2anc	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to F \in V$
12	1	qtopval	$⊢ (J \in V \land F \in V) \to J qTop F = \{s \in 𝒫 F [X] \| F^{-1} [s] \cap X \in J\}$
13	2 11 12	syl2anc	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to J qTop F = \{s \in 𝒫 F [X] \| F^{-1} [s] \cap X \in J\}$
14		imassrn	$⊢ F [X] \subseteq ran F$
15		forn	$⊢ F : Z \underset{onto}{⟶} Y \to ran F = Y$
16	15	3ad2ant2	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to ran F = Y$
17	14 16	sseqtrid	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to F [X] \subseteq Y$
18		foima	$⊢ F : Z \underset{onto}{⟶} Y \to F [Z] = Y$
19	18	3ad2ant2	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to F [Z] = Y$
20		imass2	$⊢ Z \subseteq X \to F [Z] \subseteq F [X]$
21	8 20	syl	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to F [Z] \subseteq F [X]$
22	19 21	eqsstrrd	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to Y \subseteq F [X]$
23	17 22	eqssd	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to F [X] = Y$
24	23	pweqd	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to 𝒫 F [X] = 𝒫 Y$
25		cnvimass	$⊢ F^{-1} [s] \subseteq dom F$
26	25 4	fssdm	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to F^{-1} [s] \subseteq Z$
27	26 8	sstrd	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to F^{-1} [s] \subseteq X$
28		df-ss	$⊢ F^{-1} [s] \subseteq X \leftrightarrow F^{-1} [s] \cap X = F^{-1} [s]$
29	27 28	sylib	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to F^{-1} [s] \cap X = F^{-1} [s]$
30	29	eleq1d	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to (F^{-1} [s] \cap X \in J \leftrightarrow F^{-1} [s] \in J)$
31	24 30	rabeqbidv	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to \{s \in 𝒫 F [X] \| F^{-1} [s] \cap X \in J\} = \{s \in 𝒫 Y \| F^{-1} [s] \in J\}$
32	13 31	eqtrd	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to J qTop F = \{s \in 𝒫 Y \| F^{-1} [s] \in J\}$

Metamath Proof Explorer

Theorem qtopval2

Proof