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