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 → 𝐶 ∈ 𝐴 )