Metamath Proof Explorer


Theorem tfr2b

Description: 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, 24-Jun-2015)

Ref Expression
Hypothesis tfr.1
|- F = recs ( G )
Assertion tfr2b
|- ( Ord A -> ( A e. dom F <-> ( F |` A ) e. _V ) )

Proof

Step Hyp Ref Expression
1 tfr.1
 |-  F = recs ( G )
2 ordeleqon
 |-  ( Ord A <-> ( A e. On \/ A = On ) )
3 eqid
 |-  { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) } = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }
4 3 tfrlem15
 |-  ( A e. On -> ( A e. dom recs ( G ) <-> ( recs ( G ) |` A ) e. _V ) )
5 1 dmeqi
 |-  dom F = dom recs ( G )
6 5 eleq2i
 |-  ( A e. dom F <-> A e. dom recs ( G ) )
7 1 reseq1i
 |-  ( F |` A ) = ( recs ( G ) |` A )
8 7 eleq1i
 |-  ( ( F |` A ) e. _V <-> ( recs ( G ) |` A ) e. _V )
9 4 6 8 3bitr4g
 |-  ( A e. On -> ( A e. dom F <-> ( F |` A ) e. _V ) )
10 onprc
 |-  -. On e. _V
11 elex
 |-  ( On e. dom F -> On e. _V )
12 10 11 mto
 |-  -. On e. dom F
13 eleq1
 |-  ( A = On -> ( A e. dom F <-> On e. dom F ) )
14 12 13 mtbiri
 |-  ( A = On -> -. A e. dom F )
15 3 tfrlem13
 |-  -. recs ( G ) e. _V
16 1 15 eqneltri
 |-  -. F e. _V
17 reseq2
 |-  ( A = On -> ( F |` A ) = ( F |` On ) )
18 1 tfr1a
 |-  ( Fun F /\ Lim dom F )
19 18 simpli
 |-  Fun F
20 funrel
 |-  ( Fun F -> Rel F )
21 19 20 ax-mp
 |-  Rel F
22 18 simpri
 |-  Lim dom F
23 limord
 |-  ( Lim dom F -> Ord dom F )
24 ordsson
 |-  ( Ord dom F -> dom F C_ On )
25 22 23 24 mp2b
 |-  dom F C_ On
26 relssres
 |-  ( ( Rel F /\ dom F C_ On ) -> ( F |` On ) = F )
27 21 25 26 mp2an
 |-  ( F |` On ) = F
28 17 27 eqtrdi
 |-  ( A = On -> ( F |` A ) = F )
29 28 eleq1d
 |-  ( A = On -> ( ( F |` A ) e. _V <-> F e. _V ) )
30 16 29 mtbiri
 |-  ( A = On -> -. ( F |` A ) e. _V )
31 14 30 2falsed
 |-  ( A = On -> ( A e. dom F <-> ( F |` A ) e. _V ) )
32 9 31 jaoi
 |-  ( ( A e. On \/ A = On ) -> ( A e. dom F <-> ( F |` A ) e. _V ) )
33 2 32 sylbi
 |-  ( Ord A -> ( A e. dom F <-> ( F |` A ) e. _V ) )