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

Metamath Proof Explorer

Theorem tfrlem12

Description: Lemma for transfinite recursion. Show C is an acceptable function. (Contributed by NM, 15-Aug-1994) (Revised by Mario Carneiro, 9-May-2015)

Ref Expression
Hypotheses tfrlem.1 ⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
tfrlem.3 ⊢ 𝐶 = ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } )
Assertion tfrlem12 ( recs ( 𝐹 ) ∈ V → 𝐶 ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 tfrlem.1 ⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
2 tfrlem.3 ⊢ 𝐶 = ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } )
3 1 tfrlem8 ⊢ Ord dom recs ( 𝐹 )
4 3 a1i ⊢ ( recs ( 𝐹 ) ∈ V → Ord dom recs ( 𝐹 ) )
5 dmexg ⊢ ( recs ( 𝐹 ) ∈ V → dom recs ( 𝐹 ) ∈ V )
6 elon2 ⊢ ( dom recs ( 𝐹 ) ∈ On ↔ ( Ord dom recs ( 𝐹 ) ∧ dom recs ( 𝐹 ) ∈ V ) )
7 4 5 6 sylanbrc ⊢ ( recs ( 𝐹 ) ∈ V → dom recs ( 𝐹 ) ∈ On )
8 onsuc ⊢ ( dom recs ( 𝐹 ) ∈ On → suc dom recs ( 𝐹 ) ∈ On )
9 1 2 tfrlem10 ⊢ ( dom recs ( 𝐹 ) ∈ On → 𝐶 Fn suc dom recs ( 𝐹 ) )
10 1 2 tfrlem11 ⊢ ( dom recs ( 𝐹 ) ∈ On → ( 𝑧 ∈ suc dom recs ( 𝐹 ) → ( 𝐶 ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝑧 ) ) ) )
11 10 ralrimiv ⊢ ( dom recs ( 𝐹 ) ∈ On → ∀ 𝑧 ∈ suc dom recs ( 𝐹 ) ( 𝐶 ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝑧 ) ) )
12 fveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝐶 ‘ 𝑧 ) = ( 𝐶 ‘ 𝑦 ) )
13 reseq2 ⊢ ( 𝑧 = 𝑦 → ( 𝐶 ↾ 𝑧 ) = ( 𝐶 ↾ 𝑦 ) )
14 13 fveq2d ⊢ ( 𝑧 = 𝑦 → ( 𝐹 ‘ ( 𝐶 ↾ 𝑧 ) ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝑦 ) ) )
15 12 14 eqeq12d ⊢ ( 𝑧 = 𝑦 → ( ( 𝐶 ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝑧 ) ) ↔ ( 𝐶 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝑦 ) ) ) )
16 15 cbvralvw ⊢ ( ∀ 𝑧 ∈ suc dom recs ( 𝐹 ) ( 𝐶 ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝑧 ) ) ↔ ∀ 𝑦 ∈ suc dom recs ( 𝐹 ) ( 𝐶 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝑦 ) ) )
17 11 16 sylib ⊢ ( dom recs ( 𝐹 ) ∈ On → ∀ 𝑦 ∈ suc dom recs ( 𝐹 ) ( 𝐶 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝑦 ) ) )
18 fneq2 ⊢ ( 𝑥 = suc dom recs ( 𝐹 ) → ( 𝐶 Fn 𝑥 ↔ 𝐶 Fn suc dom recs ( 𝐹 ) ) )
19 raleq ⊢ ( 𝑥 = suc dom recs ( 𝐹 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐶 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝑦 ) ) ↔ ∀ 𝑦 ∈ suc dom recs ( 𝐹 ) ( 𝐶 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝑦 ) ) ) )
20 18 19 anbi12d ⊢ ( 𝑥 = suc dom recs ( 𝐹 ) → ( ( 𝐶 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐶 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝑦 ) ) ) ↔ ( 𝐶 Fn suc dom recs ( 𝐹 ) ∧ ∀ 𝑦 ∈ suc dom recs ( 𝐹 ) ( 𝐶 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝑦 ) ) ) ) )
21 20 rspcev ⊢ ( ( suc dom recs ( 𝐹 ) ∈ On ∧ ( 𝐶 Fn suc dom recs ( 𝐹 ) ∧ ∀ 𝑦 ∈ suc dom recs ( 𝐹 ) ( 𝐶 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝑦 ) ) ) ) → ∃ 𝑥 ∈ On ( 𝐶 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐶 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝑦 ) ) ) )
22 8 9 17 21 syl12anc ⊢ ( dom recs ( 𝐹 ) ∈ On → ∃ 𝑥 ∈ On ( 𝐶 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐶 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝑦 ) ) ) )
23 7 22 syl ⊢ ( recs ( 𝐹 ) ∈ V → ∃ 𝑥 ∈ On ( 𝐶 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐶 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝑦 ) ) ) )
24 snex ⊢ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ∈ V
25 unexg ⊢ ( ( recs ( 𝐹 ) ∈ V ∧ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ∈ V ) → ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) ∈ V )
26 24 25 mpan2 ⊢ ( recs ( 𝐹 ) ∈ V → ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) ∈ V )
27 2 26 eqeltrid ⊢ ( recs ( 𝐹 ) ∈ V → 𝐶 ∈ V )
28 fneq1 ⊢ ( 𝑓 = 𝐶 → ( 𝑓 Fn 𝑥 ↔ 𝐶 Fn 𝑥 ) )
29 fveq1 ⊢ ( 𝑓 = 𝐶 → ( 𝑓 ‘ 𝑦 ) = ( 𝐶 ‘ 𝑦 ) )
30 reseq1 ⊢ ( 𝑓 = 𝐶 → ( 𝑓 ↾ 𝑦 ) = ( 𝐶 ↾ 𝑦 ) )
31 30 fveq2d ⊢ ( 𝑓 = 𝐶 → ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝑦 ) ) )
32 29 31 eqeq12d ⊢ ( 𝑓 = 𝐶 → ( ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ↔ ( 𝐶 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝑦 ) ) ) )
33 32 ralbidv ⊢ ( 𝑓 = 𝐶 → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑥 ( 𝐶 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝑦 ) ) ) )
34 28 33 anbi12d ⊢ ( 𝑓 = 𝐶 → ( ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ↔ ( 𝐶 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐶 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝑦 ) ) ) ) )
35 34 rexbidv ⊢ ( 𝑓 = 𝐶 → ( ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ↔ ∃ 𝑥 ∈ On ( 𝐶 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐶 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝑦 ) ) ) ) )
36 35 1 elab2g ⊢ ( 𝐶 ∈ V → ( 𝐶 ∈ 𝐴 ↔ ∃ 𝑥 ∈ On ( 𝐶 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐶 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝑦 ) ) ) ) )
37 27 36 syl ⊢ ( recs ( 𝐹 ) ∈ V → ( 𝐶 ∈ 𝐴 ↔ ∃ 𝑥 ∈ On ( 𝐶 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐶 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝐶 ↾ 𝑦 ) ) ) ) )
38 23 37 mpbird ⊢ ( recs ( 𝐹 ) ∈ V → 𝐶 ∈ 𝐴 )