Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  cnmptcom Unicode version

Theorem cnmptcom 12669
 Description: The argument converse of a continuous function is continuous. (Contributed by Mario Carneiro, 6-Jun-2014.)
Hypotheses
Ref Expression
cnmptcom.3 TopOn
cnmptcom.4 TopOn
cnmptcom.6
Assertion
Ref Expression
cnmptcom
Distinct variable groups:   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)   (,)   (,)

Proof of Theorem cnmptcom
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cnmptcom.3 . . . . . . . . 9 TopOn
2 cnmptcom.4 . . . . . . . . 9 TopOn
3 txtopon 12633 . . . . . . . . 9 TopOn TopOn TopOn
41, 2, 3syl2anc 409 . . . . . . . 8 TopOn
5 cnmptcom.6 . . . . . . . . . 10
6 cntop2 12573 . . . . . . . . . 10
75, 6syl 14 . . . . . . . . 9
8 toptopon2 12388 . . . . . . . . 9 TopOn
97, 8sylib 121 . . . . . . . 8 TopOn
10 cnf2 12576 . . . . . . . 8 TopOn TopOn
114, 9, 5, 10syl3anc 1220 . . . . . . 7
12 eqid 2157 . . . . . . . . 9
1312fmpo 6146 . . . . . . . 8
14 ralcom 2620 . . . . . . . 8
1513, 14bitr3i 185 . . . . . . 7
1611, 15sylib 121 . . . . . 6
17 eqid 2157 . . . . . . 7
1817fmpo 6146 . . . . . 6
1916, 18sylib 121 . . . . 5
2019ffnd 5319 . . . 4
21 fnovim 5926 . . . 4
2220, 21syl 14 . . 3
23 nfcv 2299 . . . . . . 7
24 nfcv 2299 . . . . . . 7
25 nfcv 2299 . . . . . . 7
26 nfv 1508 . . . . . . . 8
27 nfcv 2299 . . . . . . . . . 10
28 nfmpo2 5886 . . . . . . . . . 10
2927, 28, 23nfov 5848 . . . . . . . . 9
30 nfmpo1 5885 . . . . . . . . . 10
3123, 30, 27nfov 5848 . . . . . . . . 9
3229, 31nfeq 2307 . . . . . . . 8
3326, 32nfim 1552 . . . . . . 7
34 nfv 1508 . . . . . . . 8
35 nfmpo1 5885 . . . . . . . . . 10
3625, 35, 24nfov 5848 . . . . . . . . 9
37 nfmpo2 5886 . . . . . . . . . 10
3824, 37, 25nfov 5848 . . . . . . . . 9
3936, 38nfeq 2307 . . . . . . . 8
4034, 39nfim 1552 . . . . . . 7
41 oveq2 5829 . . . . . . . . 9
42 oveq1 5828 . . . . . . . . 9
4341, 42eqeq12d 2172 . . . . . . . 8
4443imbi2d 229 . . . . . . 7
45 oveq1 5828 . . . . . . . . 9
46 oveq2 5829 . . . . . . . . 9
4745, 46eqeq12d 2172 . . . . . . . 8
4847imbi2d 229 . . . . . . 7
49 rsp2 2507 . . . . . . . . 9
5049, 16syl11 31 . . . . . . . 8
5112ovmpt4g 5940 . . . . . . . . . . 11
52513com12 1189 . . . . . . . . . 10
5317ovmpt4g 5940 . . . . . . . . . 10
5452, 53eqtr4d 2193 . . . . . . . . 9
55543expia 1187 . . . . . . . 8
5650, 55syld 45 . . . . . . 7
5723, 24, 25, 33, 40, 44, 48, 56vtocl2gaf 2779 . . . . . 6
5857com12 30 . . . . 5
59583impib 1183 . . . 4
6059mpoeq3dva 5882 . . 3
6122, 60eqtr4d 2193 . 2
622, 1cnmpt2nd 12660 . . 3
632, 1cnmpt1st 12659 . . 3
642, 1, 62, 63, 5cnmpt22f 12666 . 2
6561, 64eqeltrd 2234 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   w3a 963   wceq 1335   wcel 2128  wral 2435  cuni 3772   cxp 4583   wfn 5164  wf 5165  cfv 5169  (class class class)co 5821   cmpo 5823  ctop 12366  TopOnctopon 12379   ccn 12556   ctx 12623 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-coll 4079  ax-sep 4082  ax-pow 4135  ax-pr 4169  ax-un 4393  ax-setind 4495 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-ral 2440  df-rex 2441  df-reu 2442  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-iun 3851  df-br 3966  df-opab 4026  df-mpt 4027  df-id 4253  df-xp 4591  df-rel 4592  df-cnv 4593  df-co 4594  df-dm 4595  df-rn 4596  df-res 4597  df-ima 4598  df-iota 5134  df-fun 5171  df-fn 5172  df-f 5173  df-f1 5174  df-fo 5175  df-f1o 5176  df-fv 5177  df-ov 5824  df-oprab 5825  df-mpo 5826  df-1st 6085  df-2nd 6086  df-map 6592  df-topgen 12343  df-top 12367  df-topon 12380  df-bases 12412  df-cn 12559  df-tx 12624 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator