This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem frrlem7

Description: Lemma for well-founded recursion. The well-founded recursion generator's domain is a subclass of A . (Contributed by Scott Fenton, 27-Aug-2022)

Ref Expression
Hypotheses frrlem5.1 
|- B = { 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 ) = ( y G ( f |` Pred ( R , A , y ) ) ) ) }
frrlem5.2 
|- F = frecs ( R , A , G )
Assertion frrlem7 
|- dom F C_ A

Proof

Step Hyp Ref Expression
1 frrlem5.1 
 |-  B = { 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 ) = ( y G ( f |` Pred ( R , A , y ) ) ) ) }
2 frrlem5.2 
 |-  F = frecs ( R , A , G )
3 1 2 frrlem5 
 |-  F = U. B
4 3 dmeqi 
 |-  dom F = dom U. B
5 dmuni 
 |-  dom U. B = U_ g e. B dom g
6 4 5 eqtri 
 |-  dom F = U_ g e. B dom g
7 6 sseq1i 
 |-  ( dom F C_ A <-> U_ g e. B dom g C_ A )
8 iunss 
 |-  ( U_ g e. B dom g C_ A <-> A. g e. B dom g C_ A )
9 7 8 bitri 
 |-  ( dom F C_ A <-> A. g e. B dom g C_ A )
10 1 frrlem3 
 |-  ( g e. B -> dom g C_ A )
11 9 10 mprgbir 
 |-  dom F C_ A