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

Theorem drsdirfi 14387
 Description: Any finite number of elements in a directed set have a common upper bound. Here is where the non-emptiness constraint in df-drs 14378 first comes into play; without it we would need an additional constraint that not be empty. (Contributed by Stefan O'Rear, 1-Feb-2015.)
Hypotheses
Ref Expression
drsbn0.b
drsdirfi.l
Assertion
Ref Expression
drsdirfi Dirset
Distinct variable groups:   ,,   ,,   , ,   ,,

Proof of Theorem drsdirfi
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sseq1 3361 . . . . . 6
21anbi2d 685 . . . . 5 Dirset Dirset
3 raleq 2896 . . . . . 6
43rexbidv 2718 . . . . 5
52, 4imbi12d 312 . . . 4 Dirset Dirset
6 sseq1 3361 . . . . . 6
76anbi2d 685 . . . . 5 Dirset Dirset
8 raleq 2896 . . . . . 6
98rexbidv 2718 . . . . 5
107, 9imbi12d 312 . . . 4 Dirset Dirset
11 sseq1 3361 . . . . . 6
1211anbi2d 685 . . . . 5 Dirset Dirset
13 raleq 2896 . . . . . 6
1413rexbidv 2718 . . . . 5
1512, 14imbi12d 312 . . . 4 Dirset Dirset
16 sseq1 3361 . . . . . 6
1716anbi2d 685 . . . . 5 Dirset Dirset
18 raleq 2896 . . . . . 6
1918rexbidv 2718 . . . . 5
2017, 19imbi12d 312 . . . 4 Dirset Dirset
21 drsbn0.b . . . . . . 7
2221drsbn0 14386 . . . . . 6 Dirset
23 ral0 3724 . . . . . . . . 9
2423jctr 527 . . . . . . . 8
2524eximi 1585 . . . . . . 7
26 n0 3629 . . . . . . 7
27 df-rex 2703 . . . . . . 7
2825, 26, 273imtr4i 258 . . . . . 6
2922, 28syl 16 . . . . 5 Dirset
3029adantr 452 . . . 4 Dirset
31 ssun1 3502 . . . . . . . . 9
32 sstr 3348 . . . . . . . . 9
3331, 32mpan 652 . . . . . . . 8
3433anim2i 553 . . . . . . 7 Dirset Dirset
35 breq2 4208 . . . . . . . . . 10
3635ralbidv 2717 . . . . . . . . 9
3736cbvrexv 2925 . . . . . . . 8
38 simpll 731 . . . . . . . . . . 11 Dirset Dirset
39 simprl 733 . . . . . . . . . . 11 Dirset
40 ssun2 3503 . . . . . . . . . . . . . 14
41 sstr 3348 . . . . . . . . . . . . . 14
4240, 41mpan 652 . . . . . . . . . . . . 13
43 vex 2951 . . . . . . . . . . . . . 14
4443snss 3918 . . . . . . . . . . . . 13
4542, 44sylibr 204 . . . . . . . . . . . 12
4645ad2antlr 708 . . . . . . . . . . 11 Dirset
47 drsdirfi.l . . . . . . . . . . . 12
4821, 47drsdir 14384 . . . . . . . . . . 11 Dirset
4938, 39, 46, 48syl3anc 1184 . . . . . . . . . 10 Dirset
50 simplrr 738 . . . . . . . . . . . . . 14 Dirset
51 drsprs 14385 . . . . . . . . . . . . . . . . . . 19 Dirset
5251ad5antr 715 . . . . . . . . . . . . . . . . . 18 Dirset
5333ad2antlr 708 . . . . . . . . . . . . . . . . . . . . 21 Dirset
5453adantr 452 . . . . . . . . . . . . . . . . . . . 20 Dirset
5554sselda 3340 . . . . . . . . . . . . . . . . . . 19 Dirset
5655adantr 452 . . . . . . . . . . . . . . . . . 18 Dirset
57 simp-4r 744 . . . . . . . . . . . . . . . . . 18 Dirset
58 simprl 733 . . . . . . . . . . . . . . . . . . 19 Dirset
5958ad2antrr 707 . . . . . . . . . . . . . . . . . 18 Dirset
60 simpr 448 . . . . . . . . . . . . . . . . . 18 Dirset
61 simprrl 741 . . . . . . . . . . . . . . . . . . 19 Dirset
6261ad2antrr 707 . . . . . . . . . . . . . . . . . 18 Dirset
6321, 47prstr 14382 . . . . . . . . . . . . . . . . . 18
6452, 56, 57, 59, 60, 62, 63syl132anc 1202 . . . . . . . . . . . . . . . . 17 Dirset
6564ex 424 . . . . . . . . . . . . . . . 16 Dirset
6665ralimdva 2776 . . . . . . . . . . . . . . 15 Dirset
6766adantlrr 702 . . . . . . . . . . . . . 14 Dirset
6850, 67mpd 15 . . . . . . . . . . . . 13 Dirset
69 simprrr 742 . . . . . . . . . . . . . 14 Dirset
70 breq1 4207 . . . . . . . . . . . . . . 15
7143, 70ralsn 3841 . . . . . . . . . . . . . 14
7269, 71sylibr 204 . . . . . . . . . . . . 13 Dirset
73 ralun 3521 . . . . . . . . . . . . 13
7468, 72, 73syl2anc 643 . . . . . . . . . . . 12 Dirset
7574expr 599 . . . . . . . . . . 11 Dirset
7675reximdva 2810 . . . . . . . . . 10 Dirset
7749, 76mpd 15 . . . . . . . . 9 Dirset
7877rexlimdvaa 2823 . . . . . . . 8 Dirset
7937, 78syl5bi 209 . . . . . . 7 Dirset
8034, 79embantd 52 . . . . . 6 Dirset Dirset
8180com12 29 . . . . 5 Dirset Dirset
8281a1i 11 . . . 4 Dirset Dirset
835, 10, 15, 20, 30, 82findcard2 7340 . . 3 Dirset
8483com12 29 . 2 Dirset
85843impia 1150 1 Dirset
 Colors of variables: wff set class Syntax hints:   wi 4   wa 359   w3a 936  wex 1550   wceq 1652   wcel 1725   wne 2598  wral 2697  wrex 2698   cun 3310   wss 3312  c0 3620  csn 3806   class class class wbr 4204  cfv 5446  cfn 7101  cbs 13461  cple 13528   cpreset 14375  Dirsetcdrs 14376 This theorem is referenced by:  isdrs2  14388  ipodrsfi  14581 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-1o 6716  df-er 6897  df-en 7102  df-fin 7105  df-preset 14377  df-drs 14378
 Copyright terms: Public domain W3C validator