Metamath Proof Explorer

Theorem tfrlem14

Description: Lemma for transfinite recursion. Assuming ax-rep , dom recs e.V <-> recs e. V , so since dom recs is an ordinal, it must be equal to On . (Contributed by NM, 14-Aug-1994) (Revised by Mario Carneiro, 9-May-2015)

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

Proof

Step Hyp Ref Expression
1 tfrlem.1 ⊢ A = f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = F ⁡ f ↾ y
2 1 tfrlem13 ⊢ ¬ recs ⁡ F ∈ V
3 1 tfrlem7 ⊢ Fun ⁡ recs ⁡ F
4 funex ⊢ Fun ⁡ recs ⁡ F ∧ dom ⁡ recs ⁡ F ∈ On → recs ⁡ F ∈ V
5 3 4 mpan ⊢ dom ⁡ recs ⁡ F ∈ On → recs ⁡ F ∈ V
6 2 5 mto ⊢ ¬ dom ⁡ recs ⁡ F ∈ On
7 1 tfrlem8 ⊢ Ord ⁡ dom ⁡ recs ⁡ F
8 ordeleqon ⊢ Ord ⁡ dom ⁡ recs ⁡ F ↔ dom ⁡ recs ⁡ F ∈ On ∨ dom ⁡ recs ⁡ F = On
9 7 8 mpbi ⊢ dom ⁡ recs ⁡ F ∈ On ∨ dom ⁡ recs ⁡ F = On
10 6 9 mtpor ⊢ dom ⁡ recs ⁡ F = On