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	4 9	fexd	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to F \in V$
11	1	qtopval	$⊢ (J \in V \land F \in V) \to J qTop F = \{s \in 𝒫 F [X] \| F^{-1} [s] \cap X \in J\}$
12	2 10 11	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\}$
13		imassrn	$⊢ F [X] \subseteq ran F$
14		forn	$⊢ F : Z \underset{onto}{⟶} Y \to ran F = Y$
15	14	3ad2ant2	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to ran F = Y$
16	13 15	sseqtrid	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to F [X] \subseteq Y$
17		foima	$⊢ F : Z \underset{onto}{⟶} Y \to F [Z] = Y$
18	17	3ad2ant2	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to F [Z] = Y$
19		imass2	$⊢ Z \subseteq X \to F [Z] \subseteq F [X]$
20	8 19	syl	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to F [Z] \subseteq F [X]$
21	18 20	eqsstrrd	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to Y \subseteq F [X]$
22	16 21	eqssd	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to F [X] = Y$
23	22	pweqd	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to 𝒫 F [X] = 𝒫 Y$
24		cnvimass	$⊢ F^{-1} [s] \subseteq dom F$
25	24 4	fssdm	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to F^{-1} [s] \subseteq Z$
26	25 8	sstrd	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to F^{-1} [s] \subseteq X$
27		dfss2	$⊢ F^{-1} [s] \subseteq X \leftrightarrow F^{-1} [s] \cap X = F^{-1} [s]$
28	26 27	sylib	$⊢ (J \in V \land F : Z \underset{onto}{⟶} Y \land Z \subseteq X) \to F^{-1} [s] \cap X = F^{-1} [s]$
29	28	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)$
30	23 29	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\}$
31	12 30	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