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 | |- ( H RelPres R , S ( A , B ) -> ( S Fr B -> R Fr A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id | |- ( H RelPres R , S ( A , B ) -> H RelPres R , S ( A , B ) ) |
|
| 2 | relpf | |- ( H RelPres R , S ( A , B ) -> H : A --> B ) |
|
| 3 | ffun | |- ( H : A --> B -> Fun H ) |
|
| 4 | vex | |- x e. _V |
|
| 5 | 4 | funimaex | |- ( Fun H -> ( H " x ) e. _V ) |
| 6 | 2 3 5 | 3syl | |- ( H RelPres R , S ( A , B ) -> ( H " x ) e. _V ) |
| 7 | 1 6 | relpfrlem | |- ( H RelPres R , S ( A , B ) -> ( S Fr B -> R Fr A ) ) |