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 ) ) ) )