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 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 )