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.

Step	Hyp	Ref	Expression
1		reluni 4972	. . 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 2422	. . . . 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 ) ) ) ) }
3	2	wfrlem2 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 5615	. . . 4 |- ( Fun g -> Rel g )
5	3, 4	syl 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 )
6	1, 5	mprgbir 2789	. 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 ) ) ) ) }
9	7, 8	eqtri 2451	. . 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 ) ) ) ) }
10	9	releqi 4934	. 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 ) ) ) ) } )
11	6, 10	mpbir 212	1 |- Rel F

Syntax hints:   /\ wa 370   /\ w3a 982   = wceq 1437   E.wex 1659   e. wcel 1868   {cab 2407   A.wral 2775   C_ wss 3436   U.cuni 4216   |` cres 4852   Rel wrel 4855   Predcpred 5395   Fun wfun 5592   Fn 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-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  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-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:  wfrfun  7051