Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  kqfvima Structured version   Unicode version

Theorem kqfvima 20743
 Description: When the image set is open, the quotient map satisfies a partial converse to fnfvima 6158, which is normally only true for injective functions. (Contributed by Mario Carneiro, 25-Aug-2015.)
Hypothesis
Ref Expression
kqval.2
Assertion
Ref Expression
kqfvima TopOn
Distinct variable groups:   ,,   ,,   ,,
Allowed substitution hints:   (,)   (,)

Proof of Theorem kqfvima
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 kqval.2 . . . . 5
21kqffn 20738 . . . 4 TopOn
323ad2ant1 1026 . . 3 TopOn
4 toponss 19942 . . . 4 TopOn
543adant3 1025 . . 3 TopOn
6 fnfvima 6158 . . . 4
763expia 1207 . . 3
83, 5, 7syl2anc 665 . 2 TopOn
9 fnfun 5691 . . . 4
10 fvelima 5933 . . . . 5
1110ex 435 . . . 4
123, 9, 113syl 18 . . 3 TopOn
13 simpl1 1008 . . . . . . . 8 TopOn TopOn
145sselda 3464 . . . . . . . 8 TopOn
15 simpl3 1010 . . . . . . . 8 TopOn
161kqfeq 20737 . . . . . . . 8 TopOn
1713, 14, 15, 16syl3anc 1264 . . . . . . 7 TopOn
18 eleq2 2496 . . . . . . . . 9
19 eleq2 2496 . . . . . . . . 9
2018, 19bibi12d 322 . . . . . . . 8
2120cbvralv 3054 . . . . . . 7
2217, 21syl6bb 264 . . . . . 6 TopOn
23 simpl2 1009 . . . . . . 7 TopOn
24 eleq2 2496 . . . . . . . . 9
25 eleq2 2496 . . . . . . . . 9
2624, 25bibi12d 322 . . . . . . . 8
2726rspcv 3178 . . . . . . 7
2823, 27syl 17 . . . . . 6 TopOn
2922, 28sylbid 218 . . . . 5 TopOn
30 simpr 462 . . . . 5 TopOn
31 biimp 196 . . . . 5
3229, 30, 31syl6ci 67 . . . 4 TopOn
3332rexlimdva 2914 . . 3 TopOn
3412, 33syld 45 . 2 TopOn
358, 34impbid 193 1 TopOn
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   w3a 982   wceq 1437   wcel 1872  wral 2771  wrex 2772  crab 2775   wss 3436   cmpt 4482  cima 4856   wfun 5595   wfn 5596  cfv 5601  TopOnctopon 19916 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-mpt 4484  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-fv 5609  df-topon 19921 This theorem is referenced by:  kqsat  20744  kqdisj  20745  kqcldsat  20746  kqt0lem  20749  isr0  20750  regr1lem  20752  kqreglem1  20754  kqreglem2  20755
 Copyright terms: Public domain W3C validator