Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  toplat Unicode version

Theorem toplat 25290
 Description: A topology when ordered by the inclusion is a lattice. This fact leads to the idea of pointless topology, that is a lattice looked at with the eyes of a topologist. (Contributed by FL, 6-Sep-2009.)
Hypothesis
Ref Expression
toplat.1
Assertion
Ref Expression
toplat
Distinct variable groups:   ,,   ,,

Proof of Theorem toplat
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 toplat.1 . . 3
21inposet 25278 . 2
32adantr 451 . . . . . 6
4 simprl 732 . . . . . . 7
5 vex 2791 . . . . . . . . 9
6 vex 2791 . . . . . . . . 9
75, 6prss 3769 . . . . . . . 8
8 uniopn 16643 . . . . . . . 8
97, 8sylan2b 461 . . . . . . 7
10 ssid 3197 . . . . . . . 8
115prid1 3734 . . . . . . . . 9
1211a1i 10 . . . . . . . 8
13 ssuni 3849 . . . . . . . 8
1410, 12, 13sylancr 644 . . . . . . 7
15 zfpair2 4215 . . . . . . . . 9
1615uniex 4516 . . . . . . . 8
175, 16, 1definc 25279 . . . . . . 7
184, 9, 14, 17syl3anbrc 1136 . . . . . 6
19 simprr 733 . . . . . . 7
20 ssid 3197 . . . . . . . 8
216prid2 3735 . . . . . . . . 9
2221a1i 10 . . . . . . . 8
23 ssuni 3849 . . . . . . . 8
2420, 22, 23sylancr 644 . . . . . . 7
256, 16, 1definc 25279 . . . . . . 7
2619, 9, 24, 25syl3anbrc 1136 . . . . . 6
27 vex 2791 . . . . . . . . . . 11
285, 27, 1definc 25279 . . . . . . . . . 10
296, 27, 1definc 25279 . . . . . . . . . . . . 13
30 unss 3349 . . . . . . . . . . . . . . . 16
319ad2antrl 708 . . . . . . . . . . . . . . . . . 18
32 simprr 733 . . . . . . . . . . . . . . . . . 18
335, 6unipr 3841 . . . . . . . . . . . . . . . . . . . . . 22
3433eqcomi 2287 . . . . . . . . . . . . . . . . . . . . 21
3534sseq1i 3202 . . . . . . . . . . . . . . . . . . . 20
3635biimpi 186 . . . . . . . . . . . . . . . . . . 19
3736adantr 451 . . . . . . . . . . . . . . . . . 18
3816, 27, 1definc 25279 . . . . . . . . . . . . . . . . . 18
3931, 32, 37, 38syl3anbrc 1136 . . . . . . . . . . . . . . . . 17
4039ex 423 . . . . . . . . . . . . . . . 16
4130, 40sylbi 187 . . . . . . . . . . . . . . 15
4241expcom 424 . . . . . . . . . . . . . 14
43423ad2ant3 978 . . . . . . . . . . . . 13
4429, 43sylbi 187 . . . . . . . . . . . 12
4544com12 27 . . . . . . . . . . 11
46453ad2ant3 978 . . . . . . . . . 10
4728, 46sylbi 187 . . . . . . . . 9
4847imp 418 . . . . . . . 8
4948com12 27 . . . . . . 7
5049ralrimiva 2626 . . . . . 6
511domncnt 25282 . . . . . . . 8
5251eqcomi 2287 . . . . . . 7
5352spwpr4 14340 . . . . . 6
543, 18, 26, 50, 53syl121anc 1187 . . . . 5
5554, 9eqeltrd 2357 . . . 4
56 nfwval 25245 . . . . . . 7
573, 15, 56sylancl 643 . . . . . 6
58 cnvps 14321 . . . . . . . . 9
592, 58syl 15 . . . . . . . 8
6059adantr 451 . . . . . . 7
61 simpr 447 . . . . . . . 8
625, 6intpr 3895 . . . . . . . . 9
63 inopn 16645 . . . . . . . . . 10
64633expb 1152 . . . . . . . . 9
6562, 64syl5eqel 2367 . . . . . . . 8
6662eleq1i 2346 . . . . . . . . . . . . . . 15
6766biimpi 186 . . . . . . . . . . . . . 14
6867adantl 452 . . . . . . . . . . . . 13
69 simpl 443 . . . . . . . . . . . . 13
70 inss1 3389 . . . . . . . . . . . . . 14
7170a1i 10 . . . . . . . . . . . . 13
725inex1 4155 . . . . . . . . . . . . . 14
7372, 5, 1definc 25279 . . . . . . . . . . . . 13
7468, 69, 71, 73syl3anbrc 1136 . . . . . . . . . . . 12
7562, 74syl5eqbr 4056 . . . . . . . . . . 11
76 brcnvg 4862 . . . . . . . . . . 11
7775, 76mpbird 223 . . . . . . . . . 10
7877adantlr 695 . . . . . . . . 9
79 simpr 447 . . . . . . . . . . . 12
80 simpl 443 . . . . . . . . . . . 12
81 inss2 3390 . . . . . . . . . . . . . 14
8262, 81eqsstri 3208 . . . . . . . . . . . . 13
8382a1i 10 . . . . . . . . . . . 12
845prnz 3745 . . . . . . . . . . . . . 14
85 intex 4167 . . . . . . . . . . . . . 14
8684, 85mpbi 199 . . . . . . . . . . . . 13
8786, 6, 1definc 25279 . . . . . . . . . . . 12
8879, 80, 83, 87syl3anbrc 1136 . . . . . . . . . . 11
89 brcnvg 4862 . . . . . . . . . . 11
9088, 89mpbird 223 . . . . . . . . . 10
9190adantll 694 . . . . . . . . 9
9278, 91jca 518 . . . . . . . 8
9361, 65, 92syl2anc 642 . . . . . . 7
94 brcnvg 4862 . . . . . . . . . . . . . 14
954, 94sylan 457 . . . . . . . . . . . . 13
9695biimpd 198 . . . . . . . . . . . 12
97 brcnvg 4862 . . . . . . . . . . . . . 14
9819, 97sylan 457 . . . . . . . . . . . . 13
9998biimpd 198 . . . . . . . . . . . 12
10027, 5, 1definc 25279 . . . . . . . . . . . . . 14
101100biimpi 186 . . . . . . . . . . . . 13
10227, 6, 1definc 25279 . . . . . . . . . . . . . 14
103102biimpi 186 . . . . . . . . . . . . 13
104 simprr1 1003 . . . . . . . . . . . . . . 15
10565ad2antrr 706 . . . . . . . . . . . . . . 15
106 ssin 3391 . . . . . . . . . . . . . . . . . . . . . . 23
107106biimpi 186 . . . . . . . . . . . . . . . . . . . . . 22
108107, 62syl6sseqr 3225 . . . . . . . . . . . . . . . . . . . . 21
109108expcom 424 . . . . . . . . . . . . . . . . . . . 20
1101093ad2ant3 978 . . . . . . . . . . . . . . . . . . 19
111110com12 27 . . . . . . . . . . . . . . . . . 18
1121113ad2ant3 978 . . . . . . . . . . . . . . . . 17
113112imp 418 . . . . . . . . . . . . . . . 16
114113adantl 452 . . . . . . . . . . . . . . 15
11527, 86, 1definc 25279 . . . . . . . . . . . . . . 15
116104, 105, 114, 115syl3anbrc 1136 . . . . . . . . . . . . . 14
117116ex 423 . . . . . . . . . . . . 13
118101, 103, 117syl2ani 637 . . . . . . . . . . . 12
11996, 99, 118syl2and 469 . . . . . . . . . . 11
120119imp 418 . . . . . . . . . 10
12186, 27pm3.2i 441 . . . . . . . . . . . 12
122121a1i 10 . . . . . . . . . . 11
123 brcnvg 4862 . . . . . . . . . . 11
124122, 123syl 15 . . . . . . . . . 10
125120, 124mpbird 223 . . . . . . . . 9
126125exp31 587 . . . . . . . 8
127126ralrimiv 2625 . . . . . . 7
1281ranncnt 25283 . . . . . . . . 9
129 df-rn 4700 . . . . . . . . 9
130128, 129eqtr3i 2305 . . . . . . . 8
131130spwpr4 14340 . . . . . . 7
13260, 93, 127, 131syl3anc 1182 . . . . . 6
13362a1i 10 . . . . . 6
13457, 132, 1333eqtrd 2319 . . . . 5
135134, 64eqeltrd 2357 . . . 4
13655, 135jca 518 . . 3
137136ralrimivva 2635 . 2
13852isla 14342 . 2
1392, 137, 138sylanbrc 645 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   w3a 934   wceq 1623   wcel 1684   wne 2446  wral 2543  cvv 2788   cun 3150   cin 3151   wss 3152  c0 3455  cpr 3641  cuni 3827  cint 3862   class class class wbr 4023  copab 4076   cxp 4687  ccnv 4688   cdm 4689   crn 4690  (class class class)co 5858  cps 14301   cspw 14303   cinf 14304  cla 14305  ctop 16631 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-int 3863  df-br 4024  df-opab 4078  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-iota 5219  df-fun 5257  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-riota 6304  df-ps 14306  df-spw 14308  df-nfw 14309  df-lar 14310  df-top 16636
 Copyright terms: Public domain W3C validator