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	⊢ 𝐹 = recs ( 𝐺 )
	Assertion	tfr2b	⊢ ( Ord 𝐴 → ( 𝐴 ∈ dom 𝐹 ↔ ( 𝐹 ↾ 𝐴 ) ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		tfr.1	⊢ 𝐹 = recs ( 𝐺 )
2		ordeleqon	⊢ ( Ord 𝐴 ↔ ( 𝐴 ∈ On ∨ 𝐴 = On ) )
3		eqid	⊢ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ 𝑦 ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
4	3	tfrlem15	⊢ ( 𝐴 ∈ On → ( 𝐴 ∈ dom recs ( 𝐺 ) ↔ ( recs ( 𝐺 ) ↾ 𝐴 ) ∈ V ) )
5	1	dmeqi	⊢ dom 𝐹 = dom recs ( 𝐺 )
6	5	eleq2i	⊢ ( 𝐴 ∈ dom 𝐹 ↔ 𝐴 ∈ dom recs ( 𝐺 ) )
7	1	reseq1i	⊢ ( 𝐹 ↾ 𝐴 ) = ( recs ( 𝐺 ) ↾ 𝐴 )
8	7	eleq1i	⊢ ( ( 𝐹 ↾ 𝐴 ) ∈ V ↔ ( recs ( 𝐺 ) ↾ 𝐴 ) ∈ V )
9	4 6 8	3bitr4g	⊢ ( 𝐴 ∈ On → ( 𝐴 ∈ dom 𝐹 ↔ ( 𝐹 ↾ 𝐴 ) ∈ V ) )
10		onprc	⊢ ¬ On ∈ V
11		elex	⊢ ( On ∈ dom 𝐹 → On ∈ V )
12	10 11	mto	⊢ ¬ On ∈ dom 𝐹
13		eleq1	⊢ ( 𝐴 = On → ( 𝐴 ∈ dom 𝐹 ↔ On ∈ dom 𝐹 ) )
14	12 13	mtbiri	⊢ ( 𝐴 = On → ¬ 𝐴 ∈ dom 𝐹 )
15	3	tfrlem13	⊢ ¬ recs ( 𝐺 ) ∈ V
16	1 15	eqneltri	⊢ ¬ 𝐹 ∈ V
17		reseq2	⊢ ( 𝐴 = On → ( 𝐹 ↾ 𝐴 ) = ( 𝐹 ↾ On ) )
18	1	tfr1a	⊢ ( Fun 𝐹 ∧ Lim dom 𝐹 )
19	18	simpli	⊢ Fun 𝐹
20		funrel	⊢ ( Fun 𝐹 → Rel 𝐹 )
21	19 20	ax-mp	⊢ Rel 𝐹
22	18	simpri	⊢ Lim dom 𝐹
23		limord	⊢ ( Lim dom 𝐹 → Ord dom 𝐹 )
24		ordsson	⊢ ( Ord dom 𝐹 → dom 𝐹 ⊆ On )
25	22 23 24	mp2b	⊢ dom 𝐹 ⊆ On
26		relssres	⊢ ( ( Rel 𝐹 ∧ dom 𝐹 ⊆ On ) → ( 𝐹 ↾ On ) = 𝐹 )
27	21 25 26	mp2an	⊢ ( 𝐹 ↾ On ) = 𝐹
28	17 27	eqtrdi	⊢ ( 𝐴 = On → ( 𝐹 ↾ 𝐴 ) = 𝐹 )
29	28	eleq1d	⊢ ( 𝐴 = On → ( ( 𝐹 ↾ 𝐴 ) ∈ V ↔ 𝐹 ∈ V ) )
30	16 29	mtbiri	⊢ ( 𝐴 = On → ¬ ( 𝐹 ↾ 𝐴 ) ∈ V )
31	14 30	2falsed	⊢ ( 𝐴 = On → ( 𝐴 ∈ dom 𝐹 ↔ ( 𝐹 ↾ 𝐴 ) ∈ V ) )
32	9 31	jaoi	⊢ ( ( 𝐴 ∈ On ∨ 𝐴 = On ) → ( 𝐴 ∈ dom 𝐹 ↔ ( 𝐹 ↾ 𝐴 ) ∈ V ) )
33	2 32	sylbi	⊢ ( Ord 𝐴 → ( 𝐴 ∈ dom 𝐹 ↔ ( 𝐹 ↾ 𝐴 ) ∈ V ) )

Metamath Proof Explorer

Theorem tfr2b

Proof