Theorem qtopcmplem

Description: Lemma for qtopcmp and qtopconn . (Contributed by Mario Carneiro, 24-Mar-2015)

	Ref	Expression
Hypotheses	qtopcmp.1	|- X = U. J
	qtopcmplem.1	|- ( J e. A -> J e. Top )
	qtopcmplem.2	|- ( ( J e. A /\ F : X -onto-> U. ( J qTop F ) /\ F e. ( J Cn ( J qTop F ) ) ) -> ( J qTop F ) e. A )
Assertion	qtopcmplem	|- ( ( J e. A /\ F Fn X ) -> ( J qTop F ) e. A )

Proof

Step	Hyp	Ref	Expression
1		qtopcmp.1	|- X = U. J
2		qtopcmplem.1	|- ( J e. A -> J e. Top )
3		qtopcmplem.2	|- ( ( J e. A /\ F : X -onto-> U. ( J qTop F ) /\ F e. ( J Cn ( J qTop F ) ) ) -> ( J qTop F ) e. A )
4		simpl	|- ( ( J e. A /\ F Fn X ) -> J e. A )
5		dffn4	|- ( F Fn X <-> F : X -onto-> ran F )
6	5	bilani	|- ( ( J e. A /\ F Fn X ) -> F : X -onto-> ran F )
7	1	qtopuni	|- ( ( J e. Top /\ F : X -onto-> ran F ) -> ran F = U. ( J qTop F ) )
8	2 7	sylan	|- ( ( J e. A /\ F : X -onto-> ran F ) -> ran F = U. ( J qTop F ) )
9	5 8	sylan2b	|- ( ( J e. A /\ F Fn X ) -> ran F = U. ( J qTop F ) )
10		foeq3	|- ( ran F = U. ( J qTop F ) -> ( F : X -onto-> ran F <-> F : X -onto-> U. ( J qTop F ) ) )
11	9 10	syl	|- ( ( J e. A /\ F Fn X ) -> ( F : X -onto-> ran F <-> F : X -onto-> U. ( J qTop F ) ) )
12	6 11	mpbid	|- ( ( J e. A /\ F Fn X ) -> F : X -onto-> U. ( J qTop F ) )
13	1	toptopon	|- ( J e. Top <-> J e. ( TopOn ` X ) )
14	2 13	sylib	|- ( J e. A -> J e. ( TopOn ` X ) )
15		qtopid	|- ( ( J e. ( TopOn ` X ) /\ F Fn X ) -> F e. ( J Cn ( J qTop F ) ) )
16	14 15	sylan	|- ( ( J e. A /\ F Fn X ) -> F e. ( J Cn ( J qTop F ) ) )
17	4 12 16 3	syl3anc	|- ( ( J e. A /\ F Fn X ) -> ( J qTop F ) e. A )