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

Theorem ptunhmeo 17841
 Description: Define a homeomorphism from a binary product of indexed product topologies to an indexed product topology on the union of the index sets. This is the topological analogue of . (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
ptunhmeo
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)   (,)

Proof of Theorem ptunhmeo
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ptunhmeo.g . . . . 5
2 vex 2960 . . . . . . . 8
3 vex 2960 . . . . . . . 8
42, 3op1std 6358 . . . . . . 7
52, 3op2ndd 6359 . . . . . . 7
64, 5uneq12d 3503 . . . . . 6
76mpt2mpt 6166 . . . . 5
81, 7eqtr4i 2460 . . . 4
9 xp1st 6377 . . . . . . . . . 10
109adantl 454 . . . . . . . . 9
11 ixpeq2 7077 . . . . . . . . . . . . 13
12 fvres 5746 . . . . . . . . . . . . . 14
1312unieqd 4027 . . . . . . . . . . . . 13
1411, 13mprg 2776 . . . . . . . . . . . 12
15 ptunhmeo.c . . . . . . . . . . . . . 14
16 ssun1 3511 . . . . . . . . . . . . . . 15
17 ptunhmeo.u . . . . . . . . . . . . . . 15
1816, 17syl5sseqr 3398 . . . . . . . . . . . . . 14
1915, 18ssexd 4351 . . . . . . . . . . . . 13
20 ptunhmeo.f . . . . . . . . . . . . . 14
21 fssres 5611 . . . . . . . . . . . . . 14
2220, 18, 21syl2anc 644 . . . . . . . . . . . . 13
23 ptunhmeo.k . . . . . . . . . . . . . 14
2423ptuni 17627 . . . . . . . . . . . . 13
2519, 22, 24syl2anc 644 . . . . . . . . . . . 12
2614, 25syl5eqr 2483 . . . . . . . . . . 11
27 ptunhmeo.x . . . . . . . . . . 11
2826, 27syl6eqr 2487 . . . . . . . . . 10
2928adantr 453 . . . . . . . . 9
3010, 29eleqtrrd 2514 . . . . . . . 8
31 xp2nd 6378 . . . . . . . . . 10
3231adantl 454 . . . . . . . . 9
3317eqcomd 2442 . . . . . . . . . . . . 13
34 ptunhmeo.i . . . . . . . . . . . . . 14
35 uneqdifeq 3717 . . . . . . . . . . . . . 14
3618, 34, 35syl2anc 644 . . . . . . . . . . . . 13
3733, 36mpbid 203 . . . . . . . . . . . 12
3837ixpeq1d 7075 . . . . . . . . . . 11
39 ixpeq2 7077 . . . . . . . . . . . . . 14
40 fvres 5746 . . . . . . . . . . . . . . 15
4140unieqd 4027 . . . . . . . . . . . . . 14
4239, 41mprg 2776 . . . . . . . . . . . . 13
43 ssun2 3512 . . . . . . . . . . . . . . . 16
4443, 17syl5sseqr 3398 . . . . . . . . . . . . . . 15
4515, 44ssexd 4351 . . . . . . . . . . . . . 14
46 fssres 5611 . . . . . . . . . . . . . . 15
4720, 44, 46syl2anc 644 . . . . . . . . . . . . . 14
48 ptunhmeo.l . . . . . . . . . . . . . . 15
4948ptuni 17627 . . . . . . . . . . . . . 14
5045, 47, 49syl2anc 644 . . . . . . . . . . . . 13
5142, 50syl5eqr 2483 . . . . . . . . . . . 12
52 ptunhmeo.y . . . . . . . . . . . 12
5351, 52syl6eqr 2487 . . . . . . . . . . 11
5438, 53eqtrd 2469 . . . . . . . . . 10
5554adantr 453 . . . . . . . . 9
5632, 55eleqtrrd 2514 . . . . . . . 8
5718adantr 453 . . . . . . . 8
58 undifixp 7099 . . . . . . . 8
5930, 56, 57, 58syl3anc 1185 . . . . . . 7
60 ixpfn 7069 . . . . . . 7
6159, 60syl 16 . . . . . 6
62 dffn5 5773 . . . . . 6
6361, 62sylib 190 . . . . 5
6463mpteq2dva 4296 . . . 4
658, 64syl5eq 2481 . . 3
66 ptunhmeo.j . . . 4
67 pttop 17615 . . . . . . . 8
6819, 22, 67syl2anc 644 . . . . . . 7
6923, 68syl5eqel 2521 . . . . . 6
7027toptopon 16999 . . . . . 6 TopOn
7169, 70sylib 190 . . . . 5 TopOn
72 pttop 17615 . . . . . . . 8
7345, 47, 72syl2anc 644 . . . . . . 7
7448, 73syl5eqel 2521 . . . . . 6
7552toptopon 16999 . . . . . 6 TopOn
7674, 75sylib 190 . . . . 5 TopOn
77 txtopon 17624 . . . . 5 TopOn TopOn TopOn
7871, 76, 77syl2anc 644 . . . 4 TopOn
7917eleq2d 2504 . . . . . . 7
8079biimpa 472 . . . . . 6
81 elun 3489 . . . . . 6
8280, 81sylib 190 . . . . 5
83 ixpfn 7069 . . . . . . . . . . 11
8430, 83syl 16 . . . . . . . . . 10
8584adantlr 697 . . . . . . . . 9
8653adantr 453 . . . . . . . . . . . 12
8732, 86eleqtrrd 2514 . . . . . . . . . . 11
88 ixpfn 7069 . . . . . . . . . . 11
8987, 88syl 16 . . . . . . . . . 10
9089adantlr 697 . . . . . . . . 9
9134ad2antrr 708 . . . . . . . . 9
92 simplr 733 . . . . . . . . 9
93 fvun1 5795 . . . . . . . . 9
9485, 90, 91, 92, 93syl112anc 1189 . . . . . . . 8
9594mpteq2dva 4296 . . . . . . 7
9678adantr 453 . . . . . . . 8 TopOn
974mpt2mpt 6166 . . . . . . . . 9
9871adantr 453 . . . . . . . . . 10 TopOn
9976adantr 453 . . . . . . . . . 10 TopOn
10098, 99cnmpt1st 17701 . . . . . . . . 9
10197, 100syl5eqel 2521 . . . . . . . 8
10219adantr 453 . . . . . . . . . 10
10322adantr 453 . . . . . . . . . 10
104 simpr 449 . . . . . . . . . 10
10527, 23ptpjcn 17644 . . . . . . . . . 10
106102, 103, 104, 105syl3anc 1185 . . . . . . . . 9
107 fvres 5746 . . . . . . . . . . 11
108107adantl 454 . . . . . . . . . 10
109108oveq2d 6098 . . . . . . . . 9
110106, 109eleqtrd 2513 . . . . . . . 8
111 fveq1 5728 . . . . . . . 8
11296, 101, 98, 110, 111cnmpt11 17696 . . . . . . 7
11395, 112eqeltrd 2511 . . . . . 6
11484adantlr 697 . . . . . . . . 9
11589adantlr 697 . . . . . . . . 9
11634ad2antrr 708 . . . . . . . . 9
117 simplr 733 . . . . . . . . 9
118 fvun2 5796 . . . . . . . . 9
119114, 115, 116, 117, 118syl112anc 1189 . . . . . . . 8
120119mpteq2dva 4296 . . . . . . 7
12178adantr 453 . . . . . . . 8 TopOn
1225mpt2mpt 6166 . . . . . . . . 9
12371adantr 453 . . . . . . . . . 10 TopOn
12476adantr 453 . . . . . . . . . 10 TopOn
125123, 124cnmpt2nd 17702 . . . . . . . . 9
126122, 125syl5eqel 2521 . . . . . . . 8
12745adantr 453 . . . . . . . . . 10
12847adantr 453 . . . . . . . . . 10
129 simpr 449 . . . . . . . . . 10
13052, 48ptpjcn 17644 . . . . . . . . . 10
131127, 128, 129, 130syl3anc 1185 . . . . . . . . 9
132 fvres 5746 . . . . . . . . . . 11
133132adantl 454 . . . . . . . . . 10
134133oveq2d 6098 . . . . . . . . 9
135131, 134eleqtrd 2513 . . . . . . . 8
136 fveq1 5728 . . . . . . . 8
137121, 126, 124, 135, 136cnmpt11 17696 . . . . . . 7
138120, 137eqeltrd 2511 . . . . . 6
139113, 138jaodan 762 . . . . 5
14082, 139syldan 458 . . . 4
14166, 78, 15, 20, 140ptcn 17660 . . 3
14265, 141eqeltrd 2511 . 2
14327, 52, 66, 23, 48, 1, 15, 20, 17, 34ptuncnv 17840 . . 3
144 pttop 17615 . . . . . . 7
14515, 20, 144syl2anc 644 . . . . . 6
14666, 145syl5eqel 2521 . . . . 5
147 eqid 2437 . . . . . 6
148147toptopon 16999 . . . . 5 TopOn
149146, 148sylib 190 . . . 4 TopOn
150147, 66, 23ptrescn 17672 . . . . 5
15115, 20, 18, 150syl3anc 1185 . . . 4
152147, 66, 48ptrescn 17672 . . . . 5
15315, 20, 44, 152syl3anc 1185 . . . 4
154149, 151, 153cnmpt1t 17698 . . 3
155143, 154eqeltrd 2511 . 2
156 ishmeo 17792 . 2
157142, 155, 156sylanbrc 647 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wo 359   wa 360   wceq 1653   wcel 1726  cvv 2957   cdif 3318   cun 3319   cin 3320   wss 3321  c0 3629  cop 3818  cuni 4016   cmpt 4267   cxp 4877  ccnv 4878   cres 4881   wfn 5450  wf 5451  cfv 5455  (class class class)co 6082   cmpt2 6084  c1st 6348  c2nd 6349  cixp 7064  cpt 13667  ctop 16959  TopOnctopon 16960   ccn 17289   ctx 17593   chmeo 17786 This theorem is referenced by:  xpstopnlem1  17842  ptcmpfi  17846 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-rep 4321  ax-sep 4331  ax-nul 4339  ax-pow 4378  ax-pr 4404  ax-un 4702 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2711  df-rex 2712  df-reu 2713  df-rab 2715  df-v 2959  df-sbc 3163  df-csb 3253  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3630  df-if 3741  df-pw 3802  df-sn 3821  df-pr 3822  df-tp 3823  df-op 3824  df-uni 4017  df-int 4052  df-iun 4096  df-iin 4097  df-br 4214  df-opab 4268  df-mpt 4269  df-tr 4304  df-eprel 4495  df-id 4499  df-po 4504  df-so 4505  df-fr 4542  df-we 4544  df-ord 4585  df-on 4586  df-lim 4587  df-suc 4588  df-om 4847  df-xp 4885  df-rel 4886  df-cnv 4887  df-co 4888  df-dm 4889  df-rn 4890  df-res 4891  df-ima 4892  df-iota 5419  df-fun 5457  df-fn 5458  df-f 5459  df-f1 5460  df-fo 5461  df-f1o 5462  df-fv 5463  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-1st 6350  df-2nd 6351  df-recs 6634  df-rdg 6669  df-1o 6725  df-oadd 6729  df-er 6906  df-map 7021  df-ixp 7065  df-en 7111  df-dom 7112  df-fin 7114  df-fi 7417  df-topgen 13668  df-pt 13669  df-top 16964  df-bases 16966  df-topon 16967  df-cn 17292  df-cnp 17293  df-tx 17595  df-hmeo 17788
 Copyright terms: Public domain W3C validator