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

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