This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )