Metamath Proof Explorer


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 𝐹 )