Theorem wfrresex

Description: Show without using the axiom of replacement that the restriction of the well-ordered recursion generator to a predecessor class is a set. (Contributed by Scott Fenton, 18-Nov-2024)

	Ref	Expression
Hypothesis	wfrfun.1	⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 )
Assertion	wfrresex	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		wfrfun.1	⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 )
2		wefr	⊢ ( 𝑅 We 𝐴 → 𝑅 Fr 𝐴 )
3	2	adantr	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝑅 Fr 𝐴 )
4		weso	⊢ ( 𝑅 We 𝐴 → 𝑅 Or 𝐴 )
5		sopo	⊢ ( 𝑅 Or 𝐴 → 𝑅 Po 𝐴 )
6	4 5	syl	⊢ ( 𝑅 We 𝐴 → 𝑅 Po 𝐴 )
7	6	adantr	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝑅 Po 𝐴 )
8		simpr	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝑅 Se 𝐴 )
9	3 7 8	3jca	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) )
10		df-wrecs	⊢ wrecs ( 𝑅 , 𝐴 , 𝐺 ) = frecs ( 𝑅 , 𝐴 , ( 𝐺 ∘ 2nd ) )
11	1 10	eqtri	⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , ( 𝐺 ∘ 2nd ) )
12	11	fprresex	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ∈ V )
13	9 12	sylan	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ∈ V )