Metamath Proof Explorer

Theorem wfrlem15

Description: Lemma for well-founded recursion. When z is R minimal, C is an acceptable function. This step is where the Axiom of Replacement becomes required. (Contributed by Scott Fenton, 21-Apr-2011)

Ref Expression
Hypotheses wfrlem13.1 
|- R We A
wfrlem13.2 
|- R Se A
wfrlem13.3 
|- F = wrecs ( R , A , G )
wfrlem13.4 
|- C = ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } )
Assertion wfrlem15 
|- ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> C 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 ) ) ) ) } )

Proof

Step Hyp Ref Expression
1 wfrlem13.1 
 |-  R We A
2 wfrlem13.2 
 |-  R Se A
3 wfrlem13.3 
 |-  F = wrecs ( R , A , G )
4 wfrlem13.4 
 |-  C = ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } )
5 1 2 3 4 wfrlem13 
 |-  ( z e. ( A \ dom F ) -> C Fn ( dom F u. { z } ) )
6 5 adantr 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> C Fn ( dom F u. { z } ) )
7 1 3 wfrlem10 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> Pred ( R , A , z ) = dom F )
8 eldifi 
 |-  ( z e. ( A \ dom F ) -> z e. A )
9 setlikespec 
 |-  ( ( z e. A /\ R Se A ) -> Pred ( R , A , z ) e. _V )
10 8 2 9 sylancl 
 |-  ( z e. ( A \ dom F ) -> Pred ( R , A , z ) e. _V )
11 10 adantr 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> Pred ( R , A , z ) e. _V )
12 7 11 eqeltrrd 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> dom F e. _V )
13 snex 
 |-  { z } e. _V
14 unexg 
 |-  ( ( dom F e. _V /\ { z } e. _V ) -> ( dom F u. { z } ) e. _V )
15 13 14 mpan2 
 |-  ( dom F e. _V -> ( dom F u. { z } ) e. _V )
16 fnex 
 |-  ( ( C Fn ( dom F u. { z } ) /\ ( dom F u. { z } ) e. _V ) -> C e. _V )
17 15 16 sylan2 
 |-  ( ( C Fn ( dom F u. { z } ) /\ dom F e. _V ) -> C e. _V )
18 6 12 17 syl2anc 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> C e. _V )
19 12 13 14 sylancl 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> ( dom F u. { z } ) e. _V )
20 3 wfrdmss 
 |-  dom F C_ A
21 8 snssd 
 |-  ( z e. ( A \ dom F ) -> { z } C_ A )
22 unss 
 |-  ( ( dom F C_ A /\ { z } C_ A ) <-> ( dom F u. { z } ) C_ A )
23 22 biimpi 
 |-  ( ( dom F C_ A /\ { z } C_ A ) -> ( dom F u. { z } ) C_ A )
24 20 21 23 sylancr 
 |-  ( z e. ( A \ dom F ) -> ( dom F u. { z } ) C_ A )
25 24 adantr 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> ( dom F u. { z } ) C_ A )
26 elun 
 |-  ( y e. ( dom F u. { z } ) <-> ( y e. dom F \/ y e. { z } ) )
27 velsn 
 |-  ( y e. { z } <-> y = z )
28 27 orbi2i 
 |-  ( ( y e. dom F \/ y e. { z } ) <-> ( y e. dom F \/ y = z ) )
29 26 28 bitri 
 |-  ( y e. ( dom F u. { z } ) <-> ( y e. dom F \/ y = z ) )
30 3 wfrdmcl 
 |-  ( y e. dom F -> Pred ( R , A , y ) C_ dom F )
31 ssun3 
 |-  ( Pred ( R , A , y ) C_ dom F -> Pred ( R , A , y ) C_ ( dom F u. { z } ) )
32 30 31 syl 
 |-  ( y e. dom F -> Pred ( R , A , y ) C_ ( dom F u. { z } ) )
33 32 a1i 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> ( y e. dom F -> Pred ( R , A , y ) C_ ( dom F u. { z } ) ) )
34 ssun1 
 |-  dom F C_ ( dom F u. { z } )
35 7 34 eqsstrdi 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> Pred ( R , A , z ) C_ ( dom F u. { z } ) )
36 predeq3 
 |-  ( y = z -> Pred ( R , A , y ) = Pred ( R , A , z ) )
37 36 sseq1d 
 |-  ( y = z -> ( Pred ( R , A , y ) C_ ( dom F u. { z } ) <-> Pred ( R , A , z ) C_ ( dom F u. { z } ) ) )
38 35 37 syl5ibrcom 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> ( y = z -> Pred ( R , A , y ) C_ ( dom F u. { z } ) ) )
39 33 38 jaod 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> ( ( y e. dom F \/ y = z ) -> Pred ( R , A , y ) C_ ( dom F u. { z } ) ) )
40 29 39 syl5bi 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> ( y e. ( dom F u. { z } ) -> Pred ( R , A , y ) C_ ( dom F u. { z } ) ) )
41 40 ralrimiv 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> A. y e. ( dom F u. { z } ) Pred ( R , A , y ) C_ ( dom F u. { z } ) )
42 25 41 jca 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> ( ( dom F u. { z } ) C_ A /\ A. y e. ( dom F u. { z } ) Pred ( R , A , y ) C_ ( dom F u. { z } ) ) )
43 1 2 3 4 wfrlem14 
 |-  ( z e. ( A \ dom F ) -> ( y e. ( dom F u. { z } ) -> ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) ) )
44 43 ralrimiv 
 |-  ( z e. ( A \ dom F ) -> A. y e. ( dom F u. { z } ) ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) )
45 44 adantr 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> A. y e. ( dom F u. { z } ) ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) )
46 6 42 45 3jca 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> ( C Fn ( dom F u. { z } ) /\ ( ( dom F u. { z } ) C_ A /\ A. y e. ( dom F u. { z } ) Pred ( R , A , y ) C_ ( dom F u. { z } ) ) /\ A. y e. ( dom F u. { z } ) ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) ) )
47 fneq2 
 |-  ( x = ( dom F u. { z } ) -> ( C Fn x <-> C Fn ( dom F u. { z } ) ) )
48 sseq1 
 |-  ( x = ( dom F u. { z } ) -> ( x C_ A <-> ( dom F u. { z } ) C_ A ) )
49 sseq2 
 |-  ( x = ( dom F u. { z } ) -> ( Pred ( R , A , y ) C_ x <-> Pred ( R , A , y ) C_ ( dom F u. { z } ) ) )
50 49 raleqbi1dv 
 |-  ( x = ( dom F u. { z } ) -> ( A. y e. x Pred ( R , A , y ) C_ x <-> A. y e. ( dom F u. { z } ) Pred ( R , A , y ) C_ ( dom F u. { z } ) ) )
51 48 50 anbi12d 
 |-  ( x = ( dom F u. { z } ) -> ( ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) <-> ( ( dom F u. { z } ) C_ A /\ A. y e. ( dom F u. { z } ) Pred ( R , A , y ) C_ ( dom F u. { z } ) ) ) )
52 raleq 
 |-  ( x = ( dom F u. { z } ) -> ( A. y e. x ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) <-> A. y e. ( dom F u. { z } ) ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) ) )
53 47 51 52 3anbi123d 
 |-  ( x = ( dom F u. { z } ) -> ( ( C Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) ) <-> ( C Fn ( dom F u. { z } ) /\ ( ( dom F u. { z } ) C_ A /\ A. y e. ( dom F u. { z } ) Pred ( R , A , y ) C_ ( dom F u. { z } ) ) /\ A. y e. ( dom F u. { z } ) ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) ) ) )
54 19 46 53 spcedv 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> E. x ( C Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) ) )
55 fneq1 
 |-  ( f = C -> ( f Fn x <-> C Fn x ) )
56 fveq1 
 |-  ( f = C -> ( f ` y ) = ( C ` y ) )
57 reseq1 
 |-  ( f = C -> ( f |` Pred ( R , A , y ) ) = ( C |` Pred ( R , A , y ) ) )
58 57 fveq2d 
 |-  ( f = C -> ( G ` ( f |` Pred ( R , A , y ) ) ) = ( G ` ( C |` Pred ( R , A , y ) ) ) )
59 56 58 eqeq12d 
 |-  ( f = C -> ( ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) <-> ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) ) )
60 59 ralbidv 
 |-  ( f = C -> ( A. y e. x ( f ` y ) = ( G ` ( f |` Pred ( R , A , y ) ) ) <-> A. y e. x ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) ) )
61 55 60 3anbi13d 
 |-  ( f = C -> ( ( 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 ) ) ) ) <-> ( C Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) ) ) )
62 61 exbidv 
 |-  ( f = C -> ( 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 ) ) ) ) <-> E. x ( C Fn x /\ ( x C_ A /\ A. y e. x Pred ( R , A , y ) C_ x ) /\ A. y e. x ( C ` y ) = ( G ` ( C |` Pred ( R , A , y ) ) ) ) ) )
63 18 54 62 elabd 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> C 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 ) ) ) ) } )