Metamath Proof Explorer

Theorem relwf

Description: A relation is a well-founded set iff its domain and range are. (Contributed by Eric Schmidt, 29-Sep-2025)

Ref Expression
Assertion relwf ( Rel 𝑅 → ( 𝑅 ∈ ∪ ( 𝑅1 “ On ) ↔ ( dom 𝑅 ∈ ∪ ( 𝑅1 “ On ) ∧ ran 𝑅 ∈ ∪ ( 𝑅1 “ On ) ) ) )

Proof

Step Hyp Ref Expression
1 dmwf ⊢ ( 𝑅 ∈ ∪ ( 𝑅1 “ On ) → dom 𝑅 ∈ ∪ ( 𝑅1 “ On ) )
2 rnwf ⊢ ( 𝑅 ∈ ∪ ( 𝑅1 “ On ) → ran 𝑅 ∈ ∪ ( 𝑅1 “ On ) )
3 1 2 jca ⊢ ( 𝑅 ∈ ∪ ( 𝑅1 “ On ) → ( dom 𝑅 ∈ ∪ ( 𝑅1 “ On ) ∧ ran 𝑅 ∈ ∪ ( 𝑅1 “ On ) ) )
4 xpwf ⊢ ( ( dom 𝑅 ∈ ∪ ( 𝑅1 “ On ) ∧ ran 𝑅 ∈ ∪ ( 𝑅1 “ On ) ) → ( dom 𝑅 × ran 𝑅 ) ∈ ∪ ( 𝑅1 “ On ) )
5 relssdmrn ⊢ ( Rel 𝑅 → 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) )
6 sswf ⊢ ( ( ( dom 𝑅 × ran 𝑅 ) ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) ) → 𝑅 ∈ ∪ ( 𝑅1 “ On ) )
7 5 6 sylan2 ⊢ ( ( ( dom 𝑅 × ran 𝑅 ) ∈ ∪ ( 𝑅1 “ On ) ∧ Rel 𝑅 ) → 𝑅 ∈ ∪ ( 𝑅1 “ On ) )
8 7 expcom ⊢ ( Rel 𝑅 → ( ( dom 𝑅 × ran 𝑅 ) ∈ ∪ ( 𝑅1 “ On ) → 𝑅 ∈ ∪ ( 𝑅1 “ On ) ) )
9 4 8 syl5 ⊢ ( Rel 𝑅 → ( ( dom 𝑅 ∈ ∪ ( 𝑅1 “ On ) ∧ ran 𝑅 ∈ ∪ ( 𝑅1 “ On ) ) → 𝑅 ∈ ∪ ( 𝑅1 “ On ) ) )
10 3 9 impbid2 ⊢ ( Rel 𝑅 → ( 𝑅 ∈ ∪ ( 𝑅1 “ On ) ↔ ( dom 𝑅 ∈ ∪ ( 𝑅1 “ On ) ∧ ran 𝑅 ∈ ∪ ( 𝑅1 “ On ) ) ) )