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

Metamath Proof Explorer

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 )