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

Theorem wfrfun 7051
 Description: The well-founded function generator generates a function. (Contributed by Scott Fenton, 21-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
Hypotheses
Ref Expression
wfrfun.1
wfrfun.2 Se
wfrfun.3 wrecs
Assertion
Ref Expression
wfrfun

Proof of Theorem wfrfun
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wfrfun.3 . . 3 wrecs
21wfrrel 7046 . 2
3 df-wrecs 7033 . . . . . . . . . . 11 wrecs
41, 3eqtri 2451 . . . . . . . . . 10
54eleq2i 2500 . . . . . . . . 9
6 eluni 4219 . . . . . . . . 9
75, 6bitri 252 . . . . . . . 8
8 df-br 4421 . . . . . . . 8
9 df-br 4421 . . . . . . . . . 10
109anbi1i 699 . . . . . . . . 9
1110exbii 1712 . . . . . . . 8
127, 8, 113bitr4i 280 . . . . . . 7
134eleq2i 2500 . . . . . . . . 9
14 eluni 4219 . . . . . . . . 9
1513, 14bitri 252 . . . . . . . 8
16 df-br 4421 . . . . . . . 8
17 df-br 4421 . . . . . . . . . 10
1817anbi1i 699 . . . . . . . . 9
1918exbii 1712 . . . . . . . 8
2015, 16, 193bitr4i 280 . . . . . . 7
2112, 20anbi12i 701 . . . . . 6
22 eeanv 2043 . . . . . 6
2321, 22bitr4i 255 . . . . 5
24 wfrfun.1 . . . . . . . . 9
25 wfrfun.2 . . . . . . . . 9 Se
26 eqid 2422 . . . . . . . . 9
2724, 25, 26wfrlem5 7045 . . . . . . . 8
2827impcom 431 . . . . . . 7
2928an4s 833 . . . . . 6
3029exlimivv 1767 . . . . 5
3123, 30sylbi 198 . . . 4
3231ax-gen 1665 . . 3
3332gen2 1666 . 2
34 dffun2 5608 . 2
352, 33, 34mpbir2an 928 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   w3a 982  wal 1435   wceq 1437  wex 1659   wcel 1868  cab 2407  wral 2775   wss 3436  cop 4002  cuni 4216   class class class wbr 4420   Se wse 4807   wwe 4808   cres 4852   wrel 4855  cpred 5395   wfun 5592   wfn 5593  cfv 5598  wrecscwrecs 7032 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657 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 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rmo 2783  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4765  df-po 4771  df-so 4772  df-fr 4809  df-se 4810  df-we 4811  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-pred 5396  df-iota 5562  df-fun 5600  df-fn 5601  df-fv 5606  df-wrecs 7033 This theorem is referenced by:  wfrlem12  7052  wfrlem13  7053  wfrlem17  7057  wfr1  7059  bpolylem  14089
 Copyright terms: Public domain W3C validator