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