This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )