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 ∈ dom ⁡ F ↔ F ↾ A ∈ V

Proof

Step Hyp Ref Expression
1 tfr.1 ⊢ F = recs ⁡ G
2 ordeleqon ⊢ Ord ⁡ A ↔ A ∈ On ∨ A = On
3 eqid ⊢ f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = G ⁡ f ↾ y = f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = G ⁡ f ↾ y
4 3 tfrlem15 ⊢ A ∈ On → A ∈ dom ⁡ recs ⁡ G ↔ recs ⁡ G ↾ A ∈ V
5 1 dmeqi ⊢ dom ⁡ F = dom ⁡ recs ⁡ G
6 5 eleq2i ⊢ A ∈ dom ⁡ F ↔ A ∈ dom ⁡ recs ⁡ G
7 1 reseq1i ⊢ F ↾ A = recs ⁡ G ↾ A
8 7 eleq1i ⊢ F ↾ A ∈ V ↔ recs ⁡ G ↾ A ∈ V
9 4 6 8 3bitr4g ⊢ A ∈ On → A ∈ dom ⁡ F ↔ F ↾ A ∈ V
10 onprc ⊢ ¬ On ∈ V
11 elex ⊢ On ∈ dom ⁡ F → On ∈ V
12 10 11 mto ⊢ ¬ On ∈ dom ⁡ F
13 eleq1 ⊢ A = On → A ∈ dom ⁡ F ↔ On ∈ dom ⁡ F
14 12 13 mtbiri ⊢ A = On → ¬ A ∈ dom ⁡ F
15 3 tfrlem13 ⊢ ¬ recs ⁡ G ∈ V
16 1 15 eqneltri ⊢ ¬ F ∈ 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 ⊆ On
25 22 23 24 mp2b ⊢ dom ⁡ F ⊆ On
26 relssres ⊢ Rel ⁡ F ∧ dom ⁡ F ⊆ 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 ∈ V ↔ F ∈ V
30 16 29 mtbiri ⊢ A = On → ¬ F ↾ A ∈ V
31 14 30 2falsed ⊢ A = On → A ∈ dom ⁡ F ↔ F ↾ A ∈ V
32 9 31 jaoi ⊢ A ∈ On ∨ A = On → A ∈ dom ⁡ F ↔ F ↾ A ∈ V
33 2 32 sylbi ⊢ Ord ⁡ A → A ∈ dom ⁡ F ↔ F ↾ A ∈ V