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

Theorem wfrrel 7046
Description: The well-founded recursion generator generates a relationship. (Contributed by Scott Fenton, 8-Jun-2018.)
Hypothesis
Ref Expression
wfrlem6.1  |-  F  = wrecs ( R ,  A ,  G )
Assertion
Ref Expression
wfrrel  |-  Rel  F

Proof of Theorem wfrrel
Dummy variables  f 
g  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reluni 4959 . . 3  |-  ( Rel  U. { f  |  E. x ( f  Fn  x  /\  ( x 
C_  A  /\  A. y  e.  x  Pred ( R ,  A , 
y )  C_  x
)  /\  A. y  e.  x  ( f `  y )  =  ( G `  ( f  |`  Pred ( R ,  A ,  y )
) ) ) }  <->  A. g  e.  { f  |  E. x ( f  Fn  x  /\  ( x  C_  A  /\  A. y  e.  x  Pred ( R ,  A , 
y )  C_  x
)  /\  A. y  e.  x  ( f `  y )  =  ( G `  ( f  |`  Pred ( R ,  A ,  y )
) ) ) } Rel  g )
2 eqid 2453 . . . . 5  |-  { f  |  E. x ( f  Fn  x  /\  ( x  C_  A  /\  A. y  e.  x  Pred ( R ,  A , 
y )  C_  x
)  /\  A. y  e.  x  ( f `  y )  =  ( G `  ( f  |`  Pred ( R ,  A ,  y )
) ) ) }  =  { f  |  E. x ( f  Fn  x  /\  (
x  C_  A  /\  A. y  e.  x  Pred ( R ,  A , 
y )  C_  x
)  /\  A. y  e.  x  ( f `  y )  =  ( G `  ( f  |`  Pred ( R ,  A ,  y )
) ) ) }
32wfrlem2 7041 . . . 4  |-  ( g  e.  { f  |  E. x ( f  Fn  x  /\  (
x  C_  A  /\  A. y  e.  x  Pred ( R ,  A , 
y )  C_  x
)  /\  A. y  e.  x  ( f `  y )  =  ( G `  ( f  |`  Pred ( R ,  A ,  y )
) ) ) }  ->  Fun  g )
4 funrel 5602 . . . 4  |-  ( Fun  g  ->  Rel  g )
53, 4syl 17 . . 3  |-  ( g  e.  { f  |  E. x ( f  Fn  x  /\  (
x  C_  A  /\  A. y  e.  x  Pred ( R ,  A , 
y )  C_  x
)  /\  A. y  e.  x  ( f `  y )  =  ( G `  ( f  |`  Pred ( R ,  A ,  y )
) ) ) }  ->  Rel  g )
61, 5mprgbir 2754 . 2  |-  Rel  U. { f  |  E. x ( f  Fn  x  /\  ( x 
C_  A  /\  A. y  e.  x  Pred ( R ,  A , 
y )  C_  x
)  /\  A. y  e.  x  ( f `  y )  =  ( G `  ( f  |`  Pred ( R ,  A ,  y )
) ) ) }
7 wfrlem6.1 . . . 4  |-  F  = wrecs ( R ,  A ,  G )
8 df-wrecs 7033 . . . 4  |- wrecs ( R ,  A ,  G
)  =  U. {
f  |  E. x
( f  Fn  x  /\  ( x  C_  A  /\  A. y  e.  x  Pred ( R ,  A ,  y )  C_  x )  /\  A. y  e.  x  (
f `  y )  =  ( G `  ( f  |`  Pred ( R ,  A , 
y ) ) ) ) }
97, 8eqtri 2475 . . 3  |-  F  = 
U. { f  |  E. x ( f  Fn  x  /\  (
x  C_  A  /\  A. y  e.  x  Pred ( R ,  A , 
y )  C_  x
)  /\  A. y  e.  x  ( f `  y )  =  ( G `  ( f  |`  Pred ( R ,  A ,  y )
) ) ) }
109releqi 4921 . 2  |-  ( Rel 
F  <->  Rel  U. { f  |  E. x ( f  Fn  x  /\  ( x  C_  A  /\  A. y  e.  x  Pred ( R ,  A , 
y )  C_  x
)  /\  A. y  e.  x  ( f `  y )  =  ( G `  ( f  |`  Pred ( R ,  A ,  y )
) ) ) } )
116, 10mpbir 213 1  |-  Rel  F
Colors of variables: wff setvar class
Syntax hints:    /\ wa 371    /\ w3a 986    = wceq 1446   E.wex 1665    e. wcel 1889   {cab 2439   A.wral 2739    C_ wss 3406   U.cuni 4201    |` cres 4839   Rel wrel 4842   Predcpred 5382   Fun wfun 5579    Fn wfn 5580   ` cfv 5585  wrecscwrecs 7032
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-iun 4283  df-br 4406  df-opab 4465  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-pred 5383  df-iota 5549  df-fun 5587  df-fn 5588  df-fv 5593  df-wrecs 7033
This theorem is referenced by:  wfrfun  7051
  Copyright terms: Public domain W3C validator