Metamath Proof Explorer

Theorem kqfvima

Description: When the image set is open, the quotient map satisfies a partial converse to fnfvima , which is normally only true for injective functions. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis kqval.2 
|- F = ( x e. X |-> { y e. J | x e. y } )
Assertion kqfvima 
|- ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. X ) -> ( A e. U <-> ( F ` A ) e. ( F " U ) ) )

Proof

Step Hyp Ref Expression
1 kqval.2 
 |-  F = ( x e. X |-> { y e. J | x e. y } )
2 1 kqffn 
 |-  ( J e. ( TopOn ` X ) -> F Fn X )
3 2 3ad2ant1 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. X ) -> F Fn X )
4 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J ) -> U C_ X )
5 4 3adant3 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. X ) -> U C_ X )
6 fnfvima 
 |-  ( ( F Fn X /\ U C_ X /\ A e. U ) -> ( F ` A ) e. ( F " U ) )
7 6 3expia 
 |-  ( ( F Fn X /\ U C_ X ) -> ( A e. U -> ( F ` A ) e. ( F " U ) ) )
8 3 5 7 syl2anc 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. X ) -> ( A e. U -> ( F ` A ) e. ( F " U ) ) )
9 fnfun 
 |-  ( F Fn X -> Fun F )
10 fvelima 
 |-  ( ( Fun F /\ ( F ` A ) e. ( F " U ) ) -> E. z e. U ( F ` z ) = ( F ` A ) )
11 10 ex 
 |-  ( Fun F -> ( ( F ` A ) e. ( F " U ) -> E. z e. U ( F ` z ) = ( F ` A ) ) )
12 3 9 11 3syl 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. X ) -> ( ( F ` A ) e. ( F " U ) -> E. z e. U ( F ` z ) = ( F ` A ) ) )
13 simpl1 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. X ) /\ z e. U ) -> J e. ( TopOn ` X ) )
14 5 sselda 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. X ) /\ z e. U ) -> z e. X )
15 simpl3 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. X ) /\ z e. U ) -> A e. X )
16 1 kqfeq 
 |-  ( ( J e. ( TopOn ` X ) /\ z e. X /\ A e. X ) -> ( ( F ` z ) = ( F ` A ) <-> A. y e. J ( z e. y <-> A e. y ) ) )
17 13 14 15 16 syl3anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. X ) /\ z e. U ) -> ( ( F ` z ) = ( F ` A ) <-> A. y e. J ( z e. y <-> A e. y ) ) )
18 eleq2 
 |-  ( y = w -> ( z e. y <-> z e. w ) )
19 eleq2 
 |-  ( y = w -> ( A e. y <-> A e. w ) )
20 18 19 bibi12d 
 |-  ( y = w -> ( ( z e. y <-> A e. y ) <-> ( z e. w <-> A e. w ) ) )
21 20 cbvralvw 
 |-  ( A. y e. J ( z e. y <-> A e. y ) <-> A. w e. J ( z e. w <-> A e. w ) )
22 17 21 bitrdi 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. X ) /\ z e. U ) -> ( ( F ` z ) = ( F ` A ) <-> A. w e. J ( z e. w <-> A e. w ) ) )
23 simpl2 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. X ) /\ z e. U ) -> U e. J )
24 eleq2 
 |-  ( w = U -> ( z e. w <-> z e. U ) )
25 eleq2 
 |-  ( w = U -> ( A e. w <-> A e. U ) )
26 24 25 bibi12d 
 |-  ( w = U -> ( ( z e. w <-> A e. w ) <-> ( z e. U <-> A e. U ) ) )
27 26 rspcv 
 |-  ( U e. J -> ( A. w e. J ( z e. w <-> A e. w ) -> ( z e. U <-> A e. U ) ) )
28 23 27 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. X ) /\ z e. U ) -> ( A. w e. J ( z e. w <-> A e. w ) -> ( z e. U <-> A e. U ) ) )
29 22 28 sylbid 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. X ) /\ z e. U ) -> ( ( F ` z ) = ( F ` A ) -> ( z e. U <-> A e. U ) ) )
30 simpr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. X ) /\ z e. U ) -> z e. U )
31 biimp 
 |-  ( ( z e. U <-> A e. U ) -> ( z e. U -> A e. U ) )
32 29 30 31 syl6ci 
 |-  ( ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. X ) /\ z e. U ) -> ( ( F ` z ) = ( F ` A ) -> A e. U ) )
33 32 rexlimdva 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. X ) -> ( E. z e. U ( F ` z ) = ( F ` A ) -> A e. U ) )
34 12 33 syld 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. X ) -> ( ( F ` A ) e. ( F " U ) -> A e. U ) )
35 8 34 impbid 
 |-  ( ( J e. ( TopOn ` X ) /\ U e. J /\ A e. X ) -> ( A e. U <-> ( F ` A ) e. ( F " U ) ) )