Metamath Proof Explorer

Theorem tfrlem8

Description: Lemma for transfinite recursion. The domain of recs is an ordinal. (Contributed by NM, 14-Aug-1994) (Proof shortened by Alan Sare, 11-Mar-2008)

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

Proof

Step Hyp Ref Expression
1 tfrlem.1 ⊢ A = f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = F ⁡ f ↾ y
2 1 tfrlem3 ⊢ A = g | ∃ z ∈ On g Fn z ∧ ∀ w ∈ z g ⁡ w = F ⁡ g ↾ w
3 2 abeq2i ⊢ g ∈ A ↔ ∃ z ∈ On g Fn z ∧ ∀ w ∈ z g ⁡ w = F ⁡ g ↾ w
4 fndm ⊢ g Fn z → dom ⁡ g = z
5 4 adantr ⊢ g Fn z ∧ ∀ w ∈ z g ⁡ w = F ⁡ g ↾ w → dom ⁡ g = z
6 5 eleq1d ⊢ g Fn z ∧ ∀ w ∈ z g ⁡ w = F ⁡ g ↾ w → dom ⁡ g ∈ On ↔ z ∈ On
7 6 biimprcd ⊢ z ∈ On → g Fn z ∧ ∀ w ∈ z g ⁡ w = F ⁡ g ↾ w → dom ⁡ g ∈ On
8 7 rexlimiv ⊢ ∃ z ∈ On g Fn z ∧ ∀ w ∈ z g ⁡ w = F ⁡ g ↾ w → dom ⁡ g ∈ On
9 3 8 sylbi ⊢ g ∈ A → dom ⁡ g ∈ On
10 eleq1a ⊢ dom ⁡ g ∈ On → z = dom ⁡ g → z ∈ On
11 9 10 syl ⊢ g ∈ A → z = dom ⁡ g → z ∈ On
12 11 rexlimiv ⊢ ∃ g ∈ A z = dom ⁡ g → z ∈ On
13 12 abssi ⊢ z | ∃ g ∈ A z = dom ⁡ g ⊆ On
14 ssorduni ⊢ z | ∃ g ∈ A z = dom ⁡ g ⊆ On → Ord ⁡ ⋃ z | ∃ g ∈ A z = dom ⁡ g
15 13 14 ax-mp ⊢ Ord ⁡ ⋃ z | ∃ g ∈ A z = dom ⁡ g
16 1 recsfval ⊢ recs ⁡ F = ⋃ A
17 16 dmeqi ⊢ dom ⁡ recs ⁡ F = dom ⁡ ⋃ A
18 dmuni ⊢ dom ⁡ ⋃ A = ⋃ g ∈ A dom ⁡ g
19 vex ⊢ g ∈ V
20 19 dmex ⊢ dom ⁡ g ∈ V
21 20 dfiun2 ⊢ ⋃ g ∈ A dom ⁡ g = ⋃ z | ∃ g ∈ A z = dom ⁡ g
22 17 18 21 3eqtri ⊢ dom ⁡ recs ⁡ F = ⋃ z | ∃ g ∈ A z = dom ⁡ g
23 ordeq ⊢ dom ⁡ recs ⁡ F = ⋃ z | ∃ g ∈ A z = dom ⁡ g → Ord ⁡ dom ⁡ recs ⁡ F ↔ Ord ⁡ ⋃ z | ∃ g ∈ A z = dom ⁡ g
24 22 23 ax-mp ⊢ Ord ⁡ dom ⁡ recs ⁡ F ↔ Ord ⁡ ⋃ z | ∃ g ∈ A z = dom ⁡ g
25 15 24 mpbir ⊢ Ord ⁡ dom ⁡ recs ⁡ F