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

Theorem uptx 12285
 Description: Universal property of the binary topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
Hypotheses
Ref Expression
uptx.1
uptx.2
uptx.3
uptx.4
uptx.5
uptx.6
Assertion
Ref Expression
uptx
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem uptx
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2115 . . . . 5
2 eqid 2115 . . . . 5
31, 2txcnmpt 12284 . . . 4
4 uptx.1 . . . . 5
54oveq2i 5739 . . . 4
63, 5syl6eleqr 2208 . . 3
7 uptx.2 . . . . . 6
81, 7cnf 12215 . . . . 5
9 uptx.3 . . . . . 6
101, 9cnf 12215 . . . . 5
11 ffn 5230 . . . . . . . 8
1211adantr 272 . . . . . . 7
13 fo1st 6009 . . . . . . . . . 10
14 fofn 5305 . . . . . . . . . 10
1513, 14ax-mp 7 . . . . . . . . 9
16 ssv 3085 . . . . . . . . 9
17 fnssres 5194 . . . . . . . . 9
1815, 16, 17mp2an 420 . . . . . . . 8
19 ffvelrn 5507 . . . . . . . . . . . 12
20 ffvelrn 5507 . . . . . . . . . . . 12
21 opelxpi 4531 . . . . . . . . . . . 12
2219, 20, 21syl2an 285 . . . . . . . . . . 11
2322anandirs 565 . . . . . . . . . 10
2423fmpttd 5529 . . . . . . . . 9
2524ffnd 5231 . . . . . . . 8
2624frnd 5240 . . . . . . . 8
27 fnco 5189 . . . . . . . 8
2818, 25, 26, 27mp3an2i 1303 . . . . . . 7
29 fvco3 5446 . . . . . . . . 9
3024, 29sylan 279 . . . . . . . 8
31 fveq2 5375 . . . . . . . . . . 11
32 fveq2 5375 . . . . . . . . . . 11
3331, 32opeq12d 3679 . . . . . . . . . 10
34 simpr 109 . . . . . . . . . 10
35 simpll 501 . . . . . . . . . . . 12
3635, 34ffvelrnd 5510 . . . . . . . . . . 11
37 simplr 502 . . . . . . . . . . . 12
3837, 34ffvelrnd 5510 . . . . . . . . . . 11
3936, 38opelxpd 4532 . . . . . . . . . 10
402, 33, 34, 39fvmptd3 5468 . . . . . . . . 9
4140fveq2d 5379 . . . . . . . 8
42 ffvelrn 5507 . . . . . . . . . . . 12
43 ffvelrn 5507 . . . . . . . . . . . 12
44 opelxpi 4531 . . . . . . . . . . . 12
4542, 43, 44syl2an 285 . . . . . . . . . . 11
4645anandirs 565 . . . . . . . . . 10
4746fvresd 5400 . . . . . . . . 9
48 op1stg 6002 . . . . . . . . . 10
4936, 38, 48syl2anc 406 . . . . . . . . 9
5047, 49eqtrd 2147 . . . . . . . 8
5130, 41, 503eqtrrd 2152 . . . . . . 7
5212, 28, 51eqfnfvd 5475 . . . . . 6
53 uptx.5 . . . . . . . 8
54 uptx.4 . . . . . . . . 9
5554reseq2i 4774 . . . . . . . 8
5653, 55eqtri 2135 . . . . . . 7
5756coeq1i 4658 . . . . . 6
5852, 57syl6eqr 2165 . . . . 5
598, 10, 58syl2an 285 . . . 4
60 ffn 5230 . . . . . . . 8
6160adantl 273 . . . . . . 7
62 fo2nd 6010 . . . . . . . . . 10
63 fofn 5305 . . . . . . . . . 10
6462, 63ax-mp 7 . . . . . . . . 9
65 fnssres 5194 . . . . . . . . 9
6664, 16, 65mp2an 420 . . . . . . . 8
67 fnco 5189 . . . . . . . 8
6866, 25, 26, 67mp3an2i 1303 . . . . . . 7
69 fvco3 5446 . . . . . . . . 9
7024, 69sylan 279 . . . . . . . 8
7140fveq2d 5379 . . . . . . . 8
7246fvresd 5400 . . . . . . . . 9
73 op2ndg 6003 . . . . . . . . . 10
7436, 38, 73syl2anc 406 . . . . . . . . 9
7572, 74eqtrd 2147 . . . . . . . 8
7670, 71, 753eqtrrd 2152 . . . . . . 7
7761, 68, 76eqfnfvd 5475 . . . . . 6
78 uptx.6 . . . . . . . 8
7954reseq2i 4774 . . . . . . . 8
8078, 79eqtri 2135 . . . . . . 7
8180coeq1i 4658 . . . . . 6
8277, 81syl6eqr 2165 . . . . 5
838, 10, 82syl2an 285 . . . 4
846, 59, 83jca32 306 . . 3
85 eleq1 2177 . . . . 5
86 coeq2 4657 . . . . . . 7
8786eqeq2d 2126 . . . . . 6
88 coeq2 4657 . . . . . . 7
8988eqeq2d 2126 . . . . . 6
9087, 89anbi12d 462 . . . . 5
9185, 90anbi12d 462 . . . 4
9291spcegv 2745 . . 3
936, 84, 92sylc 62 . 2
94 eqid 2115 . . . . . . . 8
951, 94cnf 12215 . . . . . . 7
96 cntop2 12213 . . . . . . . . 9
97 cntop2 12213 . . . . . . . . 9
987, 9txuni 12274 . . . . . . . . . 10
994unieqi 3712 . . . . . . . . . 10
10098, 99syl6reqr 2166 . . . . . . . . 9
10196, 97, 100syl2an 285 . . . . . . . 8
102101feq3d 5219 . . . . . . 7
10395, 102syl5ib 153 . . . . . 6
104103anim1d 332 . . . . 5
105 3anass 949 . . . . 5
106104, 105syl6ibr 161 . . . 4
107106alrimiv 1828 . . 3
108 cntop1 12212 . . . . . 6
109 uniexg 4321 . . . . . 6
110108, 109syl 14 . . . . 5
11156, 80upxp 12283 . . . . 5
112110, 8, 10, 111syl2an3an 1259 . . . 4
113 eumo 2007 . . . 4
114112, 113syl 14 . . 3
115 moim 2039 . . 3
116107, 114, 115sylc 62 . 2
117 df-reu 2397 . . 3
118 eu5 2022 . . 3
119117, 118bitri 183 . 2
12093, 116, 119sylanbrc 411 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   w3a 945  wal 1312   wceq 1314  wex 1451   wcel 1463  weu 1975  wmo 1976  wreu 2392  cvv 2657   wss 3037  cop 3496  cuni 3702   cmpt 3949   cxp 4497   crn 4500   cres 4501   ccom 4503   wfn 5076  wf 5077  wfo 5079  cfv 5081  (class class class)co 5728  c1st 5990  c2nd 5991  ctop 12007   ccn 12197   ctx 12263 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-coll 4003  ax-sep 4006  ax-pow 4058  ax-pr 4091  ax-un 4315  ax-setind 4412 This theorem depends on definitions:  df-bi 116  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-ne 2283  df-ral 2395  df-rex 2396  df-reu 2397  df-rab 2399  df-v 2659  df-sbc 2879  df-csb 2972  df-dif 3039  df-un 3041  df-in 3043  df-ss 3050  df-nul 3330  df-pw 3478  df-sn 3499  df-pr 3500  df-op 3502  df-uni 3703  df-iun 3781  df-br 3896  df-opab 3950  df-mpt 3951  df-id 4175  df-xp 4505  df-rel 4506  df-cnv 4507  df-co 4508  df-dm 4509  df-rn 4510  df-res 4511  df-ima 4512  df-iota 5046  df-fun 5083  df-fn 5084  df-f 5085  df-f1 5086  df-fo 5087  df-f1o 5088  df-fv 5089  df-ov 5731  df-oprab 5732  df-mpo 5733  df-1st 5992  df-2nd 5993  df-map 6498  df-topgen 11984  df-top 12008  df-topon 12021  df-bases 12053  df-cn 12200  df-tx 12264 This theorem is referenced by:  txcn  12286
 Copyright terms: Public domain W3C validator