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

Theorem ptuncnv 20043
 Description: Exhibit the converse function of the map which joins two product topologies on disjoint index sets. (Contributed by Mario Carneiro, 8-Feb-2015.) (Proof shortened by Mario Carneiro, 23-Aug-2015.)
Hypotheses
Ref Expression
ptunhmeo.x
ptunhmeo.y
ptunhmeo.j
ptunhmeo.k
ptunhmeo.l
ptunhmeo.g
ptunhmeo.c
ptunhmeo.f
ptunhmeo.u
ptunhmeo.i
Assertion
Ref Expression
ptuncnv
Distinct variable groups:   ,,,   ,,,   ,   ,,,   ,,,   ,,,   ,,,   ,,,   ,,,   ,   ,,,   ,,,
Allowed substitution hints:   (,)   (,)

Proof of Theorem ptuncnv
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ptunhmeo.g . . . 4
2 vex 3116 . . . . . . 7
3 vex 3116 . . . . . . 7
42, 3op1std 6791 . . . . . 6
52, 3op2ndd 6792 . . . . . 6
64, 5uneq12d 3659 . . . . 5
76mpt2mpt 6376 . . . 4
81, 7eqtr4i 2499 . . 3
9 xp1st 6811 . . . . . . 7
109adantl 466 . . . . . 6
11 ixpeq2 7480 . . . . . . . . . 10
12 fvres 5878 . . . . . . . . . . 11
1312unieqd 4255 . . . . . . . . . 10
1411, 13mprg 2827 . . . . . . . . 9
15 ptunhmeo.c . . . . . . . . . . 11
16 ssun1 3667 . . . . . . . . . . . 12
17 ptunhmeo.u . . . . . . . . . . . 12
1816, 17syl5sseqr 3553 . . . . . . . . . . 11
1915, 18ssexd 4594 . . . . . . . . . 10
20 ptunhmeo.f . . . . . . . . . . 11
21 fssres 5749 . . . . . . . . . . 11
2220, 18, 21syl2anc 661 . . . . . . . . . 10
23 ptunhmeo.k . . . . . . . . . . 11
2423ptuni 19830 . . . . . . . . . 10
2519, 22, 24syl2anc 661 . . . . . . . . 9
2614, 25syl5eqr 2522 . . . . . . . 8
27 ptunhmeo.x . . . . . . . 8
2826, 27syl6eqr 2526 . . . . . . 7
2928adantr 465 . . . . . 6
3010, 29eleqtrrd 2558 . . . . 5
31 xp2nd 6812 . . . . . . 7
3231adantl 466 . . . . . 6
3317eqcomd 2475 . . . . . . . . . 10
34 ptunhmeo.i . . . . . . . . . . 11
35 uneqdifeq 3915 . . . . . . . . . . 11
3618, 34, 35syl2anc 661 . . . . . . . . . 10
3733, 36mpbid 210 . . . . . . . . 9
3837ixpeq1d 7478 . . . . . . . 8
39 ixpeq2 7480 . . . . . . . . . . 11
40 fvres 5878 . . . . . . . . . . . 12
4140unieqd 4255 . . . . . . . . . . 11
4239, 41mprg 2827 . . . . . . . . . 10
43 ssun2 3668 . . . . . . . . . . . . 13
4443, 17syl5sseqr 3553 . . . . . . . . . . . 12
4515, 44ssexd 4594 . . . . . . . . . . 11
46 fssres 5749 . . . . . . . . . . . 12
4720, 44, 46syl2anc 661 . . . . . . . . . . 11
48 ptunhmeo.l . . . . . . . . . . . 12
4948ptuni 19830 . . . . . . . . . . 11
5045, 47, 49syl2anc 661 . . . . . . . . . 10
5142, 50syl5eqr 2522 . . . . . . . . 9
52 ptunhmeo.y . . . . . . . . 9
5351, 52syl6eqr 2526 . . . . . . . 8
5438, 53eqtrd 2508 . . . . . . 7
5554adantr 465 . . . . . 6
5632, 55eleqtrrd 2558 . . . . 5
5718adantr 465 . . . . 5
58 undifixp 7502 . . . . 5
5930, 56, 57, 58syl3anc 1228 . . . 4
60 ptunhmeo.j . . . . . . 7
6160ptuni 19830 . . . . . 6
6215, 20, 61syl2anc 661 . . . . 5
6362adantr 465 . . . 4
6459, 63eleqtrd 2557 . . 3
6518adantr 465 . . . . . 6
6662eleq2d 2537 . . . . . . 7
6766biimpar 485 . . . . . 6
68 resixp 7501 . . . . . 6
6965, 67, 68syl2anc 661 . . . . 5
7028adantr 465 . . . . 5
7169, 70eleqtrd 2557 . . . 4
7244adantr 465 . . . . . 6
73 resixp 7501 . . . . . 6
7472, 67, 73syl2anc 661 . . . . 5
7553adantr 465 . . . . 5
7674, 75eleqtrd 2557 . . . 4
77 opelxpi 5030 . . . 4
7871, 76, 77syl2anc 661 . . 3
79 eqop 6821 . . . . 5
8079ad2antrl 727 . . . 4
8167adantrl 715 . . . . . . . . 9
82 ixpfn 7472 . . . . . . . . 9
83 fnresdm 5688 . . . . . . . . 9
8481, 82, 833syl 20 . . . . . . . 8
8517reseq2d 5271 . . . . . . . . 9
8685adantr 465 . . . . . . . 8
8784, 86eqtr3d 2510 . . . . . . 7
88 resundi 5285 . . . . . . 7
8987, 88syl6eq 2524 . . . . . 6
90 uneq12 3653 . . . . . . 7
9190eqeq2d 2481 . . . . . 6
9289, 91syl5ibrcom 222 . . . . 5
93 ixpfn 7472 . . . . . . . . . . . 12
9430, 93syl 16 . . . . . . . . . . 11
9594adantrr 716 . . . . . . . . . 10
96 dffn2 5730 . . . . . . . . . 10
9795, 96sylib 196 . . . . . . . . 9
9853adantr 465 . . . . . . . . . . . . 13
9932, 98eleqtrrd 2558 . . . . . . . . . . . 12
100 ixpfn 7472 . . . . . . . . . . . 12
10199, 100syl 16 . . . . . . . . . . 11
102101adantrr 716 . . . . . . . . . 10
103 dffn2 5730 . . . . . . . . . 10
104102, 103sylib 196 . . . . . . . . 9
105 res0 5276 . . . . . . . . . . 11
106 res0 5276 . . . . . . . . . . 11
107105, 106eqtr4i 2499 . . . . . . . . . 10
10834adantr 465 . . . . . . . . . . 11
109108reseq2d 5271 . . . . . . . . . 10
110108reseq2d 5271 . . . . . . . . . 10
111107, 109, 1103eqtr4a 2534 . . . . . . . . 9
112 fresaunres1 5756 . . . . . . . . 9
11397, 104, 111, 112syl3anc 1228 . . . . . . . 8
114113eqcomd 2475 . . . . . . 7
115 fresaunres2 5755 . . . . . . . . 9
11697, 104, 111, 115syl3anc 1228 . . . . . . . 8
117116eqcomd 2475 . . . . . . 7
118114, 117jca 532 . . . . . 6
119 reseq1 5265 . . . . . . . 8
120119eqeq2d 2481 . . . . . . 7
121 reseq1 5265 . . . . . . . 8
122121eqeq2d 2481 . . . . . . 7
123120, 122anbi12d 710 . . . . . 6
124118, 123syl5ibrcom 222 . . . . 5
12592, 124impbid 191 . . . 4
12680, 125bitrd 253 . . 3
1278, 64, 78, 126f1ocnv2d 6508 . 2
128127simprd 463 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   wceq 1379   wcel 1767  cvv 3113   cdif 3473   cun 3474   cin 3475   wss 3476  c0 3785  cop 4033  cuni 4245   cmpt 4505   cxp 4997  ccnv 4998   cres 5001   wfn 5581  wf 5582  wf1o 5585  cfv 5586   cmpt2 6284  c1st 6779  c2nd 6780  cixp 7466  cpt 14690  ctop 19161 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-om 6679  df-1st 6781  df-2nd 6782  df-recs 7039  df-rdg 7073  df-1o 7127  df-oadd 7131  df-er 7308  df-ixp 7467  df-en 7514  df-fin 7517  df-fi 7867  df-topgen 14695  df-pt 14696  df-top 19166  df-bases 19168 This theorem is referenced by:  ptunhmeo  20044
 Copyright terms: Public domain W3C validator