Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wzel Structured version   Unicode version

Theorem wzel 30458
 Description: The zero of a well-founded set is a member of that set. (Contributed by Scott Fenton, 13-Jun-2018.)
Assertion
Ref Expression
wzel Se

Proof of Theorem wzel
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 weso 4787 . . . 4
2 socnv 30356 . . . 4
31, 2syl 17 . . 3
5 simp1 1005 . . . 4 Se
6 simp2 1006 . . . 4 Se Se
7 ssid 3426 . . . . 5
87a1i 11 . . . 4 Se
9 simp3 1007 . . . 4 Se
10 tz6.26 5373 . . . 4 Se
115, 6, 8, 9, 10syl22anc 1265 . . 3 Se
12 pm2.27 40 . . . . . . . . . . 11
1312ad2antll 733 . . . . . . . . . 10 Se
14 breq2 4370 . . . . . . . . . . . . 13
1514rspcev 3125 . . . . . . . . . . . 12
1615ex 435 . . . . . . . . . . 11
1716ad2antrl 732 . . . . . . . . . 10 Se
1813, 17jctird 546 . . . . . . . . 9 Se
19 vex 3025 . . . . . . . . . . . 12
20 vex 3025 . . . . . . . . . . . . 13
2120elpred 5355 . . . . . . . . . . . 12
2219, 21ax-mp 5 . . . . . . . . . . 11
2322notbii 297 . . . . . . . . . 10
24 imnan 423 . . . . . . . . . 10
2523, 24bitr4i 255 . . . . . . . . 9
2619, 20brcnv 4979 . . . . . . . . . . 11
2726notbii 297 . . . . . . . . . 10
2827anbi1i 699 . . . . . . . . 9
2918, 25, 283imtr4g 273 . . . . . . . 8 Se
3029expr 618 . . . . . . 7 Se
3130com23 81 . . . . . 6 Se
3231alimdv 1757 . . . . 5 Se
33 eq0 3720 . . . . 5
34 r19.26 2894 . . . . . 6
35 df-ral 2719 . . . . . 6
3634, 35bitr3i 254 . . . . 5
3732, 33, 363imtr4g 273 . . . 4 Se
3837reximdva 2839 . . 3 Se
3911, 38mpd 15 . 2 Se
404, 39supcl 7925 1 Se
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wa 370   w3a 982  wal 1435   wceq 1437   wcel 1872   wne 2599  wral 2714  wrex 2715  cvv 3022   wss 3379  c0 3704   class class class wbr 4366   wor 4716   Se wse 4753   wwe 4754  ccnv 4795  cpred 5341  csup 7907 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pr 4603 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-reu 2721  df-rmo 2722  df-rab 2723  df-v 3024  df-sbc 3243  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-br 4367  df-opab 4426  df-po 4717  df-so 4718  df-fr 4755  df-se 4756  df-we 4757  df-xp 4802  df-cnv 4804  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-pred 5342  df-iota 5508  df-riota 6211  df-sup 7909 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator