This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
Assertion tfrlem8 Ord dom recs ( 𝐹 )

Proof

Step Hyp Ref Expression
1 tfrlem.1 ⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
2 1 tfrlem3 ⊢ 𝐴 = { 𝑔 ∣ ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑤 ) ) ) }
3 2 eqabri ⊢ ( 𝑔 ∈ 𝐴 ↔ ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑤 ) ) ) )
4 fndm ⊢ ( 𝑔 Fn 𝑧 → dom 𝑔 = 𝑧 )
5 4 adantr ⊢ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑤 ) ) ) → dom 𝑔 = 𝑧 )
6 5 eleq1d ⊢ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑤 ) ) ) → ( dom 𝑔 ∈ On ↔ 𝑧 ∈ On ) )
7 6 biimprcd ⊢ ( 𝑧 ∈ On → ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑤 ) ) ) → dom 𝑔 ∈ On ) )
8 7 rexlimiv ⊢ ( ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑤 ) ) ) → dom 𝑔 ∈ On )
9 3 8 sylbi ⊢ ( 𝑔 ∈ 𝐴 → dom 𝑔 ∈ On )
10 eleq1a ⊢ ( dom 𝑔 ∈ On → ( 𝑧 = dom 𝑔 → 𝑧 ∈ On ) )
11 9 10 syl ⊢ ( 𝑔 ∈ 𝐴 → ( 𝑧 = dom 𝑔 → 𝑧 ∈ On ) )
12 11 rexlimiv ⊢ ( ∃ 𝑔 ∈ 𝐴 𝑧 = dom 𝑔 → 𝑧 ∈ On )
13 12 abssi ⊢ { 𝑧 ∣ ∃ 𝑔 ∈ 𝐴 𝑧 = dom 𝑔 } ⊆ On
14 ssorduni ⊢ ( { 𝑧 ∣ ∃ 𝑔 ∈ 𝐴 𝑧 = dom 𝑔 } ⊆ On → Ord ∪ { 𝑧 ∣ ∃ 𝑔 ∈ 𝐴 𝑧 = dom 𝑔 } )
15 13 14 ax-mp ⊢ Ord ∪ { 𝑧 ∣ ∃ 𝑔 ∈ 𝐴 𝑧 = dom 𝑔 }
16 1 recsfval ⊢ recs ( 𝐹 ) = ∪ 𝐴
17 16 dmeqi ⊢ dom recs ( 𝐹 ) = dom ∪ 𝐴
18 dmuni ⊢ dom ∪ 𝐴 = ∪ 𝑔 ∈ 𝐴 dom 𝑔
19 vex ⊢ 𝑔 ∈ V
20 19 dmex ⊢ dom 𝑔 ∈ V
21 20 dfiun2 ⊢ ∪ 𝑔 ∈ 𝐴 dom 𝑔 = ∪ { 𝑧 ∣ ∃ 𝑔 ∈ 𝐴 𝑧 = dom 𝑔 }
22 17 18 21 3eqtri ⊢ dom recs ( 𝐹 ) = ∪ { 𝑧 ∣ ∃ 𝑔 ∈ 𝐴 𝑧 = dom 𝑔 }
23 ordeq ⊢ ( dom recs ( 𝐹 ) = ∪ { 𝑧 ∣ ∃ 𝑔 ∈ 𝐴 𝑧 = dom 𝑔 } → ( Ord dom recs ( 𝐹 ) ↔ Ord ∪ { 𝑧 ∣ ∃ 𝑔 ∈ 𝐴 𝑧 = dom 𝑔 } ) )
24 22 23 ax-mp ⊢ ( Ord dom recs ( 𝐹 ) ↔ Ord ∪ { 𝑧 ∣ ∃ 𝑔 ∈ 𝐴 𝑧 = dom 𝑔 } )
25 15 24 mpbir ⊢ Ord dom recs ( 𝐹 )