Metamath Proof Explorer

Theorem tfrlem15

Description: Lemma for transfinite recursion. 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, 14-Nov-2014)

Ref Expression
Hypothesis tfrlem.1 ⊢ A = f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = F ⁡ f ↾ y
Assertion tfrlem15 ⊢ B ∈ On → B ∈ dom ⁡ recs ⁡ F ↔ recs ⁡ F ↾ B ∈ V

Proof

Step Hyp Ref Expression
1 tfrlem.1 ⊢ A = f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = F ⁡ f ↾ y
2 1 tfrlem9a ⊢ B ∈ dom ⁡ recs ⁡ F → recs ⁡ F ↾ B ∈ V
3 2 adantl ⊢ B ∈ On ∧ B ∈ dom ⁡ recs ⁡ F → recs ⁡ F ↾ B ∈ V
4 1 tfrlem13 ⊢ ¬ recs ⁡ F ∈ V
5 simpr ⊢ B ∈ On ∧ recs ⁡ F ↾ B ∈ V → recs ⁡ F ↾ B ∈ V
6 resss ⊢ recs ⁡ F ↾ B ⊆ recs ⁡ F
7 6 a1i ⊢ dom ⁡ recs ⁡ F ⊆ B → recs ⁡ F ↾ B ⊆ recs ⁡ F
8 1 tfrlem6 ⊢ Rel ⁡ recs ⁡ F
9 resdm ⊢ Rel ⁡ recs ⁡ F → recs ⁡ F ↾ dom ⁡ recs ⁡ F = recs ⁡ F
10 8 9 ax-mp ⊢ recs ⁡ F ↾ dom ⁡ recs ⁡ F = recs ⁡ F
11 ssres2 ⊢ dom ⁡ recs ⁡ F ⊆ B → recs ⁡ F ↾ dom ⁡ recs ⁡ F ⊆ recs ⁡ F ↾ B
12 10 11 eqsstrrid ⊢ dom ⁡ recs ⁡ F ⊆ B → recs ⁡ F ⊆ recs ⁡ F ↾ B
13 7 12 eqssd ⊢ dom ⁡ recs ⁡ F ⊆ B → recs ⁡ F ↾ B = recs ⁡ F
14 13 eleq1d ⊢ dom ⁡ recs ⁡ F ⊆ B → recs ⁡ F ↾ B ∈ V ↔ recs ⁡ F ∈ V
15 5 14 syl5ibcom ⊢ B ∈ On ∧ recs ⁡ F ↾ B ∈ V → dom ⁡ recs ⁡ F ⊆ B → recs ⁡ F ∈ V
16 4 15 mtoi ⊢ B ∈ On ∧ recs ⁡ F ↾ B ∈ V → ¬ dom ⁡ recs ⁡ F ⊆ B
17 1 tfrlem8 ⊢ Ord ⁡ dom ⁡ recs ⁡ F
18 eloni ⊢ B ∈ On → Ord ⁡ B
19 18 adantr ⊢ B ∈ On ∧ recs ⁡ F ↾ B ∈ V → Ord ⁡ B
20 ordtri1 ⊢ Ord ⁡ dom ⁡ recs ⁡ F ∧ Ord ⁡ B → dom ⁡ recs ⁡ F ⊆ B ↔ ¬ B ∈ dom ⁡ recs ⁡ F
21 20 con2bid ⊢ Ord ⁡ dom ⁡ recs ⁡ F ∧ Ord ⁡ B → B ∈ dom ⁡ recs ⁡ F ↔ ¬ dom ⁡ recs ⁡ F ⊆ B
22 17 19 21 sylancr ⊢ B ∈ On ∧ recs ⁡ F ↾ B ∈ V → B ∈ dom ⁡ recs ⁡ F ↔ ¬ dom ⁡ recs ⁡ F ⊆ B
23 16 22 mpbird ⊢ B ∈ On ∧ recs ⁡ F ↾ B ∈ V → B ∈ dom ⁡ recs ⁡ F
24 3 23 impbida ⊢ B ∈ On → B ∈ dom ⁡ recs ⁡ F ↔ recs ⁡ F ↾ B ∈ V