Metamath Proof Explorer

Theorem tfrlem13

Description: Lemma for transfinite recursion. If recs is a set function, then C is acceptable, and thus a subset of recs , but dom C is bigger than dom recs . This is a contradiction, so recs must be a proper class function. (Contributed by NM, 14-Aug-1994) (Revised by Mario Carneiro, 14-Nov-2014)

Ref Expression
Hypothesis tfrlem.1 
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
Assertion tfrlem13 
|- -. recs ( F ) e. _V

Proof

Step Hyp Ref Expression
1 tfrlem.1 
 |-  A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
2 1 tfrlem8 
 |-  Ord dom recs ( F )
3 ordirr 
 |-  ( Ord dom recs ( F ) -> -. dom recs ( F ) e. dom recs ( F ) )
4 2 3 ax-mp 
 |-  -. dom recs ( F ) e. dom recs ( F )
5 eqid 
 |-  ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) = ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )
6 1 5 tfrlem12 
 |-  ( recs ( F ) e. _V -> ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) e. A )
7 elssuni 
 |-  ( ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) e. A -> ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) C_ U. A )
8 1 recsfval 
 |-  recs ( F ) = U. A
9 7 8 sseqtrrdi 
 |-  ( ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) e. A -> ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) C_ recs ( F ) )
10 dmss 
 |-  ( ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) C_ recs ( F ) -> dom ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) C_ dom recs ( F ) )
11 6 9 10 3syl 
 |-  ( recs ( F ) e. _V -> dom ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) C_ dom recs ( F ) )
12 2 a1i 
 |-  ( recs ( F ) e. _V -> Ord dom recs ( F ) )
13 dmexg 
 |-  ( recs ( F ) e. _V -> dom recs ( F ) e. _V )
14 elon2 
 |-  ( dom recs ( F ) e. On <-> ( Ord dom recs ( F ) /\ dom recs ( F ) e. _V ) )
15 12 13 14 sylanbrc 
 |-  ( recs ( F ) e. _V -> dom recs ( F ) e. On )
16 sucidg 
 |-  ( dom recs ( F ) e. On -> dom recs ( F ) e. suc dom recs ( F ) )
17 15 16 syl 
 |-  ( recs ( F ) e. _V -> dom recs ( F ) e. suc dom recs ( F ) )
18 1 5 tfrlem10 
 |-  ( dom recs ( F ) e. On -> ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) Fn suc dom recs ( F ) )
19 fndm 
 |-  ( ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) Fn suc dom recs ( F ) -> dom ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) = suc dom recs ( F ) )
20 15 18 19 3syl 
 |-  ( recs ( F ) e. _V -> dom ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) = suc dom recs ( F ) )
21 17 20 eleqtrrd 
 |-  ( recs ( F ) e. _V -> dom recs ( F ) e. dom ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) )
22 11 21 sseldd 
 |-  ( recs ( F ) e. _V -> dom recs ( F ) e. dom recs ( F ) )
23 4 22 mto 
 |-  -. recs ( F ) e. _V