Metamath Proof Explorer

Theorem qtopt1

Description: If every equivalence class is closed, then the quotient space is T_1 . (Contributed by Thierry Arnoux, 5-Jan-2020)

Ref Expression
Hypotheses qtopt1.x 
|- X = U. J
qtopt1.1 
|- ( ph -> J e. Fre )
qtopt1.2 
|- ( ph -> F : X -onto-> Y )
qtopt1.3 
|- ( ( ph /\ x e. Y ) -> ( `' F " { x } ) e. ( Clsd ` J ) )
Assertion qtopt1 
|- ( ph -> ( J qTop F ) e. Fre )

Proof

Step Hyp Ref Expression
1 qtopt1.x 
 |-  X = U. J
2 qtopt1.1 
 |-  ( ph -> J e. Fre )
3 qtopt1.2 
 |-  ( ph -> F : X -onto-> Y )
4 qtopt1.3 
 |-  ( ( ph /\ x e. Y ) -> ( `' F " { x } ) e. ( Clsd ` J ) )
5 t1top 
 |-  ( J e. Fre -> J e. Top )
6 2 5 syl 
 |-  ( ph -> J e. Top )
7 fofn 
 |-  ( F : X -onto-> Y -> F Fn X )
8 3 7 syl 
 |-  ( ph -> F Fn X )
9 1 qtoptop 
 |-  ( ( J e. Top /\ F Fn X ) -> ( J qTop F ) e. Top )
10 6 8 9 syl2anc 
 |-  ( ph -> ( J qTop F ) e. Top )
11 simpr 
 |-  ( ( ph /\ x e. U. ( J qTop F ) ) -> x e. U. ( J qTop F ) )
12 1 qtopuni 
 |-  ( ( J e. Top /\ F : X -onto-> Y ) -> Y = U. ( J qTop F ) )
13 6 3 12 syl2anc 
 |-  ( ph -> Y = U. ( J qTop F ) )
14 13 adantr 
 |-  ( ( ph /\ x e. U. ( J qTop F ) ) -> Y = U. ( J qTop F ) )
15 11 14 eleqtrrd 
 |-  ( ( ph /\ x e. U. ( J qTop F ) ) -> x e. Y )
16 15 snssd 
 |-  ( ( ph /\ x e. U. ( J qTop F ) ) -> { x } C_ Y )
17 15 4 syldan 
 |-  ( ( ph /\ x e. U. ( J qTop F ) ) -> ( `' F " { x } ) e. ( Clsd ` J ) )
18 6 1 jctir 
 |-  ( ph -> ( J e. Top /\ X = U. J ) )
19 istopon 
 |-  ( J e. ( TopOn ` X ) <-> ( J e. Top /\ X = U. J ) )
20 18 19 sylibr 
 |-  ( ph -> J e. ( TopOn ` X ) )
21 qtopcld 
 |-  ( ( J e. ( TopOn ` X ) /\ F : X -onto-> Y ) -> ( { x } e. ( Clsd ` ( J qTop F ) ) <-> ( { x } C_ Y /\ ( `' F " { x } ) e. ( Clsd ` J ) ) ) )
22 20 3 21 syl2anc 
 |-  ( ph -> ( { x } e. ( Clsd ` ( J qTop F ) ) <-> ( { x } C_ Y /\ ( `' F " { x } ) e. ( Clsd ` J ) ) ) )
23 22 adantr 
 |-  ( ( ph /\ x e. U. ( J qTop F ) ) -> ( { x } e. ( Clsd ` ( J qTop F ) ) <-> ( { x } C_ Y /\ ( `' F " { x } ) e. ( Clsd ` J ) ) ) )
24 16 17 23 mpbir2and 
 |-  ( ( ph /\ x e. U. ( J qTop F ) ) -> { x } e. ( Clsd ` ( J qTop F ) ) )
25 24 ralrimiva 
 |-  ( ph -> A. x e. U. ( J qTop F ) { x } e. ( Clsd ` ( J qTop F ) ) )
26 eqid 
 |-  U. ( J qTop F ) = U. ( J qTop F )
27 26 ist1 
 |-  ( ( J qTop F ) e. Fre <-> ( ( J qTop F ) e. Top /\ A. x e. U. ( J qTop F ) { x } e. ( Clsd ` ( J qTop F ) ) ) )
28 10 25 27 sylanbrc 
 |-  ( ph -> ( J qTop F ) e. Fre )