kqfvima

Description: When the image set is open, the quotient map satisfies a partial converse to fnfvima , which is normally only true for injective functions. (Contributed by Mario Carneiro, 25-Aug-2015)

		Ref	Expression
	Hypothesis	kqval.2	$⊢ F = (x \in X ⟼ \{y \in J \| x \in y\})$
	Assertion	kqfvima	$⊢ (J \in TopOn (X) \land U \in J \land A \in X) \to (A \in U \leftrightarrow F (A) \in F [U])$

Proof

Step	Hyp	Ref	Expression
1		kqval.2	$⊢ F = (x \in X ⟼ \{y \in J \| x \in y\})$
2	1	kqffn	$⊢ J \in TopOn (X) \to F Fn X$
3	2	3ad2ant1	$⊢ (J \in TopOn (X) \land U \in J \land A \in X) \to F Fn X$
4		toponss	$⊢ (J \in TopOn (X) \land U \in J) \to U \subseteq X$
5	4	3adant3	$⊢ (J \in TopOn (X) \land U \in J \land A \in X) \to U \subseteq X$
6		fnfvima	$⊢ (F Fn X \land U \subseteq X \land A \in U) \to F (A) \in F [U]$
7	6	3expia	$⊢ (F Fn X \land U \subseteq X) \to (A \in U \to F (A) \in F [U])$
8	3 5 7	syl2anc	$⊢ (J \in TopOn (X) \land U \in J \land A \in X) \to (A \in U \to F (A) \in F [U])$
9		fnfun	$⊢ F Fn X \to Fun F$
10		fvelima	$⊢ (Fun F \land F (A) \in F [U]) \to \exists z \in U F (z) = F (A)$
11	10	ex	$⊢ Fun F \to (F (A) \in F [U] \to \exists z \in U F (z) = F (A))$
12	3 9 11	3syl	$⊢ (J \in TopOn (X) \land U \in J \land A \in X) \to (F (A) \in F [U] \to \exists z \in U F (z) = F (A))$
13		simpl1	$⊢ ((J \in TopOn (X) \land U \in J \land A \in X) \land z \in U) \to J \in TopOn (X)$
14	5	sselda	$⊢ ((J \in TopOn (X) \land U \in J \land A \in X) \land z \in U) \to z \in X$
15		simpl3	$⊢ ((J \in TopOn (X) \land U \in J \land A \in X) \land z \in U) \to A \in X$
16	1	kqfeq	$⊢ (J \in TopOn (X) \land z \in X \land A \in X) \to (F (z) = F (A) \leftrightarrow \forall y \in J (z \in y \leftrightarrow A \in y))$
17	13 14 15 16	syl3anc	$⊢ ((J \in TopOn (X) \land U \in J \land A \in X) \land z \in U) \to (F (z) = F (A) \leftrightarrow \forall y \in J (z \in y \leftrightarrow A \in y))$
18		eleq2	$⊢ y = w \to (z \in y \leftrightarrow z \in w)$
19		eleq2	$⊢ y = w \to (A \in y \leftrightarrow A \in w)$
20	18 19	bibi12d	$⊢ y = w \to ((z \in y \leftrightarrow A \in y) \leftrightarrow (z \in w \leftrightarrow A \in w))$
21	20	cbvralvw	$⊢ \forall y \in J (z \in y \leftrightarrow A \in y) \leftrightarrow \forall w \in J (z \in w \leftrightarrow A \in w)$
22	17 21	bitrdi	$⊢ ((J \in TopOn (X) \land U \in J \land A \in X) \land z \in U) \to (F (z) = F (A) \leftrightarrow \forall w \in J (z \in w \leftrightarrow A \in w))$
23		simpl2	$⊢ ((J \in TopOn (X) \land U \in J \land A \in X) \land z \in U) \to U \in J$
24		eleq2	$⊢ w = U \to (z \in w \leftrightarrow z \in U)$
25		eleq2	$⊢ w = U \to (A \in w \leftrightarrow A \in U)$
26	24 25	bibi12d	$⊢ w = U \to ((z \in w \leftrightarrow A \in w) \leftrightarrow (z \in U \leftrightarrow A \in U))$
27	26	rspcv	$⊢ U \in J \to (\forall w \in J (z \in w \leftrightarrow A \in w) \to (z \in U \leftrightarrow A \in U))$
28	23 27	syl	$⊢ ((J \in TopOn (X) \land U \in J \land A \in X) \land z \in U) \to (\forall w \in J (z \in w \leftrightarrow A \in w) \to (z \in U \leftrightarrow A \in U))$
29	22 28	sylbid	$⊢ ((J \in TopOn (X) \land U \in J \land A \in X) \land z \in U) \to (F (z) = F (A) \to (z \in U \leftrightarrow A \in U))$
30		simpr	$⊢ ((J \in TopOn (X) \land U \in J \land A \in X) \land z \in U) \to z \in U$
31		biimp	$⊢ (z \in U \leftrightarrow A \in U) \to (z \in U \to A \in U)$
32	29 30 31	syl6ci	$⊢ ((J \in TopOn (X) \land U \in J \land A \in X) \land z \in U) \to (F (z) = F (A) \to A \in U)$
33	32	rexlimdva	$⊢ (J \in TopOn (X) \land U \in J \land A \in X) \to (\exists z \in U F (z) = F (A) \to A \in U)$
34	12 33	syld	$⊢ (J \in TopOn (X) \land U \in J \land A \in X) \to (F (A) \in F [U] \to A \in U)$
35	8 34	impbid	$⊢ (J \in TopOn (X) \land U \in J \land A \in X) \to (A \in U \leftrightarrow F (A) \in F [U])$

Metamath Proof Explorer

Theorem kqfvima

Proof