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

Theorem brwdom2 7988
 Description: Alternate characterization of the weak dominance predicate which does not require special treatment of the empty set. (Contributed by Stefan O'Rear, 11-Feb-2015.)
Assertion
Ref Expression
brwdom2 *
Distinct variable groups:   ,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem brwdom2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3115 . 2
2 0wdom 7985 . . . . . 6 *
3 breq1 4443 . . . . . 6 * *
42, 3syl5ibrcom 222 . . . . 5 *
54imp 429 . . . 4 *
6 0elpw 4609 . . . . . . 7
7 f1o0 5841 . . . . . . . 8
8 f1ofo 5814 . . . . . . . 8
9 0ex 4570 . . . . . . . . 9
10 foeq1 5782 . . . . . . . . 9
119, 10spcev 3198 . . . . . . . 8
127, 8, 11mp2b 10 . . . . . . 7
13 foeq2 5783 . . . . . . . . 9
1413exbidv 1685 . . . . . . . 8
1514rspcev 3207 . . . . . . 7
166, 12, 15mp2an 672 . . . . . 6
17 foeq3 5784 . . . . . . . 8
1817exbidv 1685 . . . . . . 7
1918rexbidv 2966 . . . . . 6
2016, 19mpbiri 233 . . . . 5
2120adantl 466 . . . 4
225, 212thd 240 . . 3 *
23 brwdomn0 7984 . . . . 5 *
2423adantl 466 . . . 4 *
25 foeq1 5782 . . . . . . 7
2625cbvexv 1990 . . . . . 6
27 pwidg 4016 . . . . . . . . 9
2827ad2antrr 725 . . . . . . . 8
29 foeq2 5783 . . . . . . . . . 10
3029exbidv 1685 . . . . . . . . 9
3130rspcev 3207 . . . . . . . 8
3228, 31sylancom 667 . . . . . . 7
3332ex 434 . . . . . 6
3426, 33syl5bi 217 . . . . 5
35 n0 3787 . . . . . . . . . . 11
3635biimpi 194 . . . . . . . . . 10
3736ad2antlr 726 . . . . . . . . 9
38 vex 3109 . . . . . . . . . . . . 13
39 difexg 4588 . . . . . . . . . . . . . 14
40 snex 4681 . . . . . . . . . . . . . 14
41 xpexg 6702 . . . . . . . . . . . . . 14
4239, 40, 41sylancl 662 . . . . . . . . . . . . 13
43 unexg 6576 . . . . . . . . . . . . 13
4438, 42, 43sylancr 663 . . . . . . . . . . . 12
4544adantr 465 . . . . . . . . . . 11
4645ad2antrr 725 . . . . . . . . . 10
47 fofn 5788 . . . . . . . . . . . . . . 15
4847adantl 466 . . . . . . . . . . . . . 14
4948ad2antlr 726 . . . . . . . . . . . . 13
50 vex 3109 . . . . . . . . . . . . . 14
51 fnconstg 5764 . . . . . . . . . . . . . 14
5250, 51mp1i 12 . . . . . . . . . . . . 13
53 disjdif 3892 . . . . . . . . . . . . . 14
5453a1i 11 . . . . . . . . . . . . 13
55 fnun 5678 . . . . . . . . . . . . 13
5649, 52, 54, 55syl21anc 1222 . . . . . . . . . . . 12
57 elpwi 4012 . . . . . . . . . . . . . . . 16
58 undif 3900 . . . . . . . . . . . . . . . 16
5957, 58sylib 196 . . . . . . . . . . . . . . 15
6059ad2antrl 727 . . . . . . . . . . . . . 14
6160adantr 465 . . . . . . . . . . . . 13
6261fneq2d 5663 . . . . . . . . . . . 12
6356, 62mpbid 210 . . . . . . . . . . 11
64 rnun 5405 . . . . . . . . . . . 12
65 forn 5789 . . . . . . . . . . . . . . . 16
6665ad2antll 728 . . . . . . . . . . . . . . 15
6766adantr 465 . . . . . . . . . . . . . 14
6867uneq1d 3650 . . . . . . . . . . . . 13
69 fconst6g 5765 . . . . . . . . . . . . . . . 16
70 frn 5728 . . . . . . . . . . . . . . . 16
7169, 70syl 16 . . . . . . . . . . . . . . 15
7271adantl 466 . . . . . . . . . . . . . 14
73 ssequn2 3670 . . . . . . . . . . . . . 14
7472, 73sylib 196 . . . . . . . . . . . . 13
7568, 74eqtrd 2501 . . . . . . . . . . . 12
7664, 75syl5eq 2513 . . . . . . . . . . 11
77 df-fo 5585 . . . . . . . . . . 11
7863, 76, 77sylanbrc 664 . . . . . . . . . 10
79 foeq1 5782 . . . . . . . . . . 11
8079spcegv 3192 . . . . . . . . . 10
8146, 78, 80sylc 60 . . . . . . . . 9
8237, 81exlimddv 1697 . . . . . . . 8
8382expr 615 . . . . . . 7
8483exlimdv 1695 . . . . . 6
8584rexlimdva 2948 . . . . 5
8634, 85impbid 191 . . . 4
8724, 86bitrd 253 . . 3 *
8822, 87pm2.61dane 2778 . 2 *
891, 88syl 16 1 *
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   wceq 1374  wex 1591   wcel 1762   wne 2655  wrex 2808  cvv 3106   cdif 3466   cun 3467   cin 3468   wss 3469  c0 3778  cpw 4003  csn 4020   class class class wbr 4440   cxp 4990   crn 4993   wfn 5574  wf 5575  wfo 5577  wf1o 5578   * cwdom 7972 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-wdom 7974 This theorem is referenced by:  brwdom3  7997
 Copyright terms: Public domain W3C validator