qtopcmplem

	Ref	Expression
Hypotheses	qtopcmp.1	$⊢ X = ⋃ J$
	qtopcmplem.1	$⊢ J \in A \to J \in Top$
	qtopcmplem.2	$⊢ (J \in A \land F : X \underset{onto}{⟶} ⋃ (J qTop F) \land F \in (J Cn (J qTop F))) \to J qTop F \in A$
Assertion	qtopcmplem	$⊢ (J \in A \land F Fn X) \to J qTop F \in A$

Step	Hyp	Ref	Expression
1		qtopcmp.1	$⊢ X = ⋃ J$
2		qtopcmplem.1	$⊢ J \in A \to J \in Top$
3		qtopcmplem.2	$⊢ (J \in A \land F : X \underset{onto}{⟶} ⋃ (J qTop F) \land F \in (J Cn (J qTop F))) \to J qTop F \in A$
4		simpl	$⊢ (J \in A \land F Fn X) \to J \in A$
5		simpr	$⊢ (J \in A \land F Fn X) \to F Fn X$
6		dffn4	$⊢ F Fn X \leftrightarrow F : X \underset{onto}{⟶} ran F$
7	5 6	sylib	$⊢ (J \in A \land F Fn X) \to F : X \underset{onto}{⟶} ran F$
8	1	qtopuni	$⊢ (J \in Top \land F : X \underset{onto}{⟶} ran F) \to ran F = ⋃ (J qTop F)$
9	2 8	sylan	$⊢ (J \in A \land F : X \underset{onto}{⟶} ran F) \to ran F = ⋃ (J qTop F)$
10	6 9	sylan2b	$⊢ (J \in A \land F Fn X) \to ran F = ⋃ (J qTop F)$
11		foeq3	$⊢ ran F = ⋃ (J qTop F) \to (F : X \underset{onto}{⟶} ran F \leftrightarrow F : X \underset{onto}{⟶} ⋃ (J qTop F))$
12	10 11	syl	$⊢ (J \in A \land F Fn X) \to (F : X \underset{onto}{⟶} ran F \leftrightarrow F : X \underset{onto}{⟶} ⋃ (J qTop F))$
13	7 12	mpbid	$⊢ (J \in A \land F Fn X) \to F : X \underset{onto}{⟶} ⋃ (J qTop F)$
14	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
15	2 14	sylib	$⊢ J \in A \to J \in TopOn (X)$
16		qtopid	$⊢ (J \in TopOn (X) \land F Fn X) \to F \in (J Cn (J qTop F))$
17	15 16	sylan	$⊢ (J \in A \land F Fn X) \to F \in (J Cn (J qTop F))$
18	4 13 17 3	syl3anc	$⊢ (J \in A \land F Fn X) \to J qTop F \in A$

Metamath Proof Explorer