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

Metamath Proof Explorer

Theorem tfrlem16

Description: Lemma for finite recursion. Without assuming ax-rep , we can show that the domain of the constructed function is a limit ordinal, and hence contains all the finite ordinals. (Contributed by Mario Carneiro, 14-Nov-2014)

Ref Expression
Hypothesis tfrlem.1 ⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
Assertion tfrlem16 Lim dom recs ( 𝐹 )

Proof

Step Hyp Ref Expression
1 tfrlem.1 ⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
2 1 tfrlem8 ⊢ Ord dom recs ( 𝐹 )
3 ordzsl ⊢ ( Ord dom recs ( 𝐹 ) ↔ ( dom recs ( 𝐹 ) = ∅ ∨ ∃ 𝑧 ∈ On dom recs ( 𝐹 ) = suc 𝑧 ∨ Lim dom recs ( 𝐹 ) ) )
4 2 3 mpbi ⊢ ( dom recs ( 𝐹 ) = ∅ ∨ ∃ 𝑧 ∈ On dom recs ( 𝐹 ) = suc 𝑧 ∨ Lim dom recs ( 𝐹 ) )
5 res0 ⊢ ( recs ( 𝐹 ) ↾ ∅ ) = ∅
6 0ex ⊢ ∅ ∈ V
7 5 6 eqeltri ⊢ ( recs ( 𝐹 ) ↾ ∅ ) ∈ V
8 0elon ⊢ ∅ ∈ On
9 1 tfrlem15 ⊢ ( ∅ ∈ On → ( ∅ ∈ dom recs ( 𝐹 ) ↔ ( recs ( 𝐹 ) ↾ ∅ ) ∈ V ) )
10 8 9 ax-mp ⊢ ( ∅ ∈ dom recs ( 𝐹 ) ↔ ( recs ( 𝐹 ) ↾ ∅ ) ∈ V )
11 7 10 mpbir ⊢ ∅ ∈ dom recs ( 𝐹 )
12 11 n0ii ⊢ ¬ dom recs ( 𝐹 ) = ∅
13 12 pm2.21i ⊢ ( dom recs ( 𝐹 ) = ∅ → Lim dom recs ( 𝐹 ) )
14 1 tfrlem13 ⊢ ¬ recs ( 𝐹 ) ∈ V
15 simpr ⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → dom recs ( 𝐹 ) = suc 𝑧 )
16 df-suc ⊢ suc 𝑧 = ( 𝑧 ∪ { 𝑧 } )
17 15 16 eqtrdi ⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → dom recs ( 𝐹 ) = ( 𝑧 ∪ { 𝑧 } ) )
18 17 reseq2d ⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → ( recs ( 𝐹 ) ↾ dom recs ( 𝐹 ) ) = ( recs ( 𝐹 ) ↾ ( 𝑧 ∪ { 𝑧 } ) ) )
19 1 tfrlem6 ⊢ Rel recs ( 𝐹 )
20 resdm ⊢ ( Rel recs ( 𝐹 ) → ( recs ( 𝐹 ) ↾ dom recs ( 𝐹 ) ) = recs ( 𝐹 ) )
21 19 20 ax-mp ⊢ ( recs ( 𝐹 ) ↾ dom recs ( 𝐹 ) ) = recs ( 𝐹 )
22 resundi ⊢ ( recs ( 𝐹 ) ↾ ( 𝑧 ∪ { 𝑧 } ) ) = ( ( recs ( 𝐹 ) ↾ 𝑧 ) ∪ ( recs ( 𝐹 ) ↾ { 𝑧 } ) )
23 18 21 22 3eqtr3g ⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → recs ( 𝐹 ) = ( ( recs ( 𝐹 ) ↾ 𝑧 ) ∪ ( recs ( 𝐹 ) ↾ { 𝑧 } ) ) )
24 vex ⊢ 𝑧 ∈ V
25 24 sucid ⊢ 𝑧 ∈ suc 𝑧
26 25 15 eleqtrrid ⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → 𝑧 ∈ dom recs ( 𝐹 ) )
27 1 tfrlem9a ⊢ ( 𝑧 ∈ dom recs ( 𝐹 ) → ( recs ( 𝐹 ) ↾ 𝑧 ) ∈ V )
28 26 27 syl ⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → ( recs ( 𝐹 ) ↾ 𝑧 ) ∈ V )
29 snex ⊢ { ⟨ 𝑧 , ( recs ( 𝐹 ) ‘ 𝑧 ) ⟩ } ∈ V
30 1 tfrlem7 ⊢ Fun recs ( 𝐹 )
31 funressn ⊢ ( Fun recs ( 𝐹 ) → ( recs ( 𝐹 ) ↾ { 𝑧 } ) ⊆ { ⟨ 𝑧 , ( recs ( 𝐹 ) ‘ 𝑧 ) ⟩ } )
32 30 31 ax-mp ⊢ ( recs ( 𝐹 ) ↾ { 𝑧 } ) ⊆ { ⟨ 𝑧 , ( recs ( 𝐹 ) ‘ 𝑧 ) ⟩ }
33 29 32 ssexi ⊢ ( recs ( 𝐹 ) ↾ { 𝑧 } ) ∈ V
34 unexg ⊢ ( ( ( recs ( 𝐹 ) ↾ 𝑧 ) ∈ V ∧ ( recs ( 𝐹 ) ↾ { 𝑧 } ) ∈ V ) → ( ( recs ( 𝐹 ) ↾ 𝑧 ) ∪ ( recs ( 𝐹 ) ↾ { 𝑧 } ) ) ∈ V )
35 28 33 34 sylancl ⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → ( ( recs ( 𝐹 ) ↾ 𝑧 ) ∪ ( recs ( 𝐹 ) ↾ { 𝑧 } ) ) ∈ V )
36 23 35 eqeltrd ⊢ ( ( 𝑧 ∈ On ∧ dom recs ( 𝐹 ) = suc 𝑧 ) → recs ( 𝐹 ) ∈ V )
37 36 rexlimiva ⊢ ( ∃ 𝑧 ∈ On dom recs ( 𝐹 ) = suc 𝑧 → recs ( 𝐹 ) ∈ V )
38 14 37 mto ⊢ ¬ ∃ 𝑧 ∈ On dom recs ( 𝐹 ) = suc 𝑧
39 38 pm2.21i ⊢ ( ∃ 𝑧 ∈ On dom recs ( 𝐹 ) = suc 𝑧 → Lim dom recs ( 𝐹 ) )
40 id ⊢ ( Lim dom recs ( 𝐹 ) → Lim dom recs ( 𝐹 ) )
41 13 39 40 3jaoi ⊢ ( ( dom recs ( 𝐹 ) = ∅ ∨ ∃ 𝑧 ∈ On dom recs ( 𝐹 ) = suc 𝑧 ∨ Lim dom recs ( 𝐹 ) ) → Lim dom recs ( 𝐹 ) )
42 4 41 ax-mp ⊢ Lim dom recs ( 𝐹 )