Theorem wfrfun

Description: The "function" generated by the well-ordered recursion generator is indeed a function. Avoids the axiom of replacement. (Contributed by Scott Fenton, 21-Apr-2011) (Revised by Mario Carneiro, 26-Jun-2015) (Revised by Scott Fenton, 17-Nov-2024)

	Ref	Expression
Hypothesis	wfrfun.1	⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 )
Assertion	wfrfun	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → Fun 𝐹 )

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		df-wrecs	⊢ wrecs ( 𝑅 , 𝐴 , 𝐺 ) = frecs ( 𝑅 , 𝐴 , ( 𝐺 ∘ 2nd ) )
10	1 9	eqtri	⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , ( 𝐺 ∘ 2nd ) )
11	10	fprfung	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) → Fun 𝐹 )
12	3 7 8 11	syl3anc	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → Fun 𝐹 )