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