Metamath Proof Explorer


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 Could not format assertion : No typesetting found for |- ( H RelPres R , S ( A , B ) -> ( S Fr B -> R Fr A ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 id Could not format ( H RelPres R , S ( A , B ) -> H RelPres R , S ( A , B ) ) : No typesetting found for |- ( H RelPres R , S ( A , B ) -> H RelPres R , S ( A , B ) ) with typecode |-
2 relpf Could not format ( H RelPres R , S ( A , B ) -> H : A --> B ) : No typesetting found for |- ( H RelPres R , S ( A , B ) -> H : A --> B ) with typecode |-
3 ffun H : A B Fun H
4 vex x V
5 4 funimaex Fun H H x V
6 2 3 5 3syl Could not format ( H RelPres R , S ( A , B ) -> ( H " x ) e. _V ) : No typesetting found for |- ( H RelPres R , S ( A , B ) -> ( H " x ) e. _V ) with typecode |-
7 1 6 relpfrlem Could not format ( H RelPres R , S ( A , B ) -> ( S Fr B -> R Fr A ) ) : No typesetting found for |- ( H RelPres R , S ( A , B ) -> ( S Fr B -> R Fr A ) ) with typecode |-