Metamath Proof Explorer

Theorem tfrlem15

Description: Lemma for transfinite recursion. Without assuming ax-rep , we can show that all proper initial subsets of recs are sets, while nothing larger is a set. (Contributed 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 tfrlem15 
|- ( B e. On -> ( B e. dom recs ( F ) <-> ( recs ( F ) |` B ) 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 tfrlem9a 
 |-  ( B e. dom recs ( F ) -> ( recs ( F ) |` B ) e. _V )
3 2 adantl 
 |-  ( ( B e. On /\ B e. dom recs ( F ) ) -> ( recs ( F ) |` B ) e. _V )
4 1 tfrlem13 
 |-  -. recs ( F ) e. _V
5 simpr 
 |-  ( ( B e. On /\ ( recs ( F ) |` B ) e. _V ) -> ( recs ( F ) |` B ) e. _V )
6 resss 
 |-  ( recs ( F ) |` B ) C_ recs ( F )
7 6 a1i 
 |-  ( dom recs ( F ) C_ B -> ( recs ( F ) |` B ) C_ recs ( F ) )
8 1 tfrlem6 
 |-  Rel recs ( F )
9 resdm 
 |-  ( Rel recs ( F ) -> ( recs ( F ) |` dom recs ( F ) ) = recs ( F ) )
10 8 9 ax-mp 
 |-  ( recs ( F ) |` dom recs ( F ) ) = recs ( F )
11 ssres2 
 |-  ( dom recs ( F ) C_ B -> ( recs ( F ) |` dom recs ( F ) ) C_ ( recs ( F ) |` B ) )
12 10 11 eqsstrrid 
 |-  ( dom recs ( F ) C_ B -> recs ( F ) C_ ( recs ( F ) |` B ) )
13 7 12 eqssd 
 |-  ( dom recs ( F ) C_ B -> ( recs ( F ) |` B ) = recs ( F ) )
14 13 eleq1d 
 |-  ( dom recs ( F ) C_ B -> ( ( recs ( F ) |` B ) e. _V <-> recs ( F ) e. _V ) )
15 5 14 syl5ibcom 
 |-  ( ( B e. On /\ ( recs ( F ) |` B ) e. _V ) -> ( dom recs ( F ) C_ B -> recs ( F ) e. _V ) )
16 4 15 mtoi 
 |-  ( ( B e. On /\ ( recs ( F ) |` B ) e. _V ) -> -. dom recs ( F ) C_ B )
17 1 tfrlem8 
 |-  Ord dom recs ( F )
18 eloni 
 |-  ( B e. On -> Ord B )
19 18 adantr 
 |-  ( ( B e. On /\ ( recs ( F ) |` B ) e. _V ) -> Ord B )
20 ordtri1 
 |-  ( ( Ord dom recs ( F ) /\ Ord B ) -> ( dom recs ( F ) C_ B <-> -. B e. dom recs ( F ) ) )
21 20 con2bid 
 |-  ( ( Ord dom recs ( F ) /\ Ord B ) -> ( B e. dom recs ( F ) <-> -. dom recs ( F ) C_ B ) )
22 17 19 21 sylancr 
 |-  ( ( B e. On /\ ( recs ( F ) |` B ) e. _V ) -> ( B e. dom recs ( F ) <-> -. dom recs ( F ) C_ B ) )
23 16 22 mpbird 
 |-  ( ( B e. On /\ ( recs ( F ) |` B ) e. _V ) -> B e. dom recs ( F ) )
24 3 23 impbida 
 |-  ( B e. On -> ( B e. dom recs ( F ) <-> ( recs ( F ) |` B ) e. _V ) )