Theorem relpfr

Description: If the image of a set under a relation-preserving function is well-founded, so is the set. See isofr for a bidirectional statement. A more general version of Lemma I.9.9 of Kunen2 p. 47. (Contributed by Eric Schmidt, 11-Oct-2025)

	Ref	Expression
Assertion	relpfr	⊢ ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝑆 Fr 𝐵 → 𝑅 Fr 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
2		relpf	⊢ ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 : 𝐴 ⟶ 𝐵 )
3		ffun	⊢ ( 𝐻 : 𝐴 ⟶ 𝐵 → Fun 𝐻 )
4		vex	⊢ 𝑥 ∈ V
5	4	funimaex	⊢ ( Fun 𝐻 → ( 𝐻 “ 𝑥 ) ∈ V )
6	2 3 5	3syl	⊢ ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝐻 “ 𝑥 ) ∈ V )
7	1 6	relpfrlem	⊢ ( 𝐻 RelPres 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝑆 Fr 𝐵 → 𝑅 Fr 𝐴 ) )