Theorem wfr2a

Description: A weak version of wfr2 which is useful for proofs that avoid the Axiom of Replacement. (Contributed by Scott Fenton, 30-Jul-2020) (Proof shortened by Scott Fenton, 18-Nov-2024)

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

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	fpr2a	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝑋 ( 𝐺 ∘ 2nd ) ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) )
13	9 12	sylan	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝑋 ( 𝐺 ∘ 2nd ) ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) )
14		simpr	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) → 𝑋 ∈ dom 𝐹 )
15	1	wfrresex	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) → ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ∈ V )
16	14 15	opco2	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) → ( 𝑋 ( 𝐺 ∘ 2nd ) ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) )
17	13 16	eqtrd	⊢ ( ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑋 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑋 ) = ( 𝐺 ‘ ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) )