Metamath Proof Explorer

Theorem wfrlem16

Description: Lemma for well-founded recursion. If z is R minimal in ( A \ dom F ) , then C is acceptable and thus a subset of F , but dom C is bigger than dom F . Thus, z cannot be minimal, so ( A \ dom F ) must be empty, and (due to wfrdmss ), dom F = A . (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 wfrlem16 
|- dom F = A

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 3 wfrdmss 
 |-  dom F C_ A
6 eldifn 
 |-  ( z e. ( A \ dom F ) -> -. z e. dom F )
7 ssun2 
 |-  { z } C_ ( dom F u. { z } )
8 vsnid 
 |-  z e. { z }
9 7 8 sselii 
 |-  z e. ( dom F u. { z } )
10 4 dmeqi 
 |-  dom C = dom ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } )
11 dmun 
 |-  dom ( F u. { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } ) = ( dom F u. dom { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } )
12 fvex 
 |-  ( G ` ( F |` Pred ( R , A , z ) ) ) e. _V
13 12 dmsnop 
 |-  dom { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } = { z }
14 13 uneq2i 
 |-  ( dom F u. dom { <. z , ( G ` ( F |` Pred ( R , A , z ) ) ) >. } ) = ( dom F u. { z } )
15 10 11 14 3eqtri 
 |-  dom C = ( dom F u. { z } )
16 9 15 eleqtrri 
 |-  z e. dom C
17 1 2 3 4 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 ) ) ) ) } )
18 elssuni 
 |-  ( 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 ) ) ) ) } -> C C_ 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 ) ) ) ) } )
19 17 18 syl 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> C C_ 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 ) ) ) ) } )
20 df-wrecs 
 |-  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 ) ) ) ) }
21 3 20 eqtri 
 |-  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 ) ) ) ) }
22 19 21 sseqtrrdi 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> C C_ F )
23 dmss 
 |-  ( C C_ F -> dom C C_ dom F )
24 22 23 syl 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> dom C C_ dom F )
25 24 sseld 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> ( z e. dom C -> z e. dom F ) )
26 16 25 mpi 
 |-  ( ( z e. ( A \ dom F ) /\ Pred ( R , ( A \ dom F ) , z ) = (/) ) -> z e. dom F )
27 6 26 mtand 
 |-  ( z e. ( A \ dom F ) -> -. Pred ( R , ( A \ dom F ) , z ) = (/) )
28 27 nrex 
 |-  -. E. z e. ( A \ dom F ) Pred ( R , ( A \ dom F ) , z ) = (/)
29 df-ne 
 |-  ( ( A \ dom F ) =/= (/) <-> -. ( A \ dom F ) = (/) )
30 difss 
 |-  ( A \ dom F ) C_ A
31 1 2 tz6.26i 
 |-  ( ( ( A \ dom F ) C_ A /\ ( A \ dom F ) =/= (/) ) -> E. z e. ( A \ dom F ) Pred ( R , ( A \ dom F ) , z ) = (/) )
32 30 31 mpan 
 |-  ( ( A \ dom F ) =/= (/) -> E. z e. ( A \ dom F ) Pred ( R , ( A \ dom F ) , z ) = (/) )
33 29 32 sylbir 
 |-  ( -. ( A \ dom F ) = (/) -> E. z e. ( A \ dom F ) Pred ( R , ( A \ dom F ) , z ) = (/) )
34 28 33 mt3 
 |-  ( A \ dom F ) = (/)
35 ssdif0 
 |-  ( A C_ dom F <-> ( A \ dom F ) = (/) )
36 34 35 mpbir 
 |-  A C_ dom F
37 5 36 eqssi 
 |-  dom F = A