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 ⁡ R → R ∈ ⋃ R1 On ↔ dom ⁡ R ∈ ⋃ R1 On ∧ ran ⁡ R ∈ ⋃ R1 On

Proof

Step Hyp Ref Expression
1 dmwf ⊢ R ∈ ⋃ R1 On → dom ⁡ R ∈ ⋃ R1 On
2 rnwf ⊢ R ∈ ⋃ R1 On → ran ⁡ R ∈ ⋃ R1 On
3 1 2 jca ⊢ R ∈ ⋃ R1 On → dom ⁡ R ∈ ⋃ R1 On ∧ ran ⁡ R ∈ ⋃ R1 On
4 xpwf ⊢ dom ⁡ R ∈ ⋃ R1 On ∧ ran ⁡ R ∈ ⋃ R1 On → dom ⁡ R × ran ⁡ R ∈ ⋃ R1 On
5 relssdmrn ⊢ Rel ⁡ R → R ⊆ dom ⁡ R × ran ⁡ R
6 sswf ⊢ dom ⁡ R × ran ⁡ R ∈ ⋃ R1 On ∧ R ⊆ dom ⁡ R × ran ⁡ R → R ∈ ⋃ R1 On
7 5 6 sylan2 ⊢ dom ⁡ R × ran ⁡ R ∈ ⋃ R1 On ∧ Rel ⁡ R → R ∈ ⋃ R1 On
8 7 expcom ⊢ Rel ⁡ R → dom ⁡ R × ran ⁡ R ∈ ⋃ R1 On → R ∈ ⋃ R1 On
9 4 8 syl5 ⊢ Rel ⁡ R → dom ⁡ R ∈ ⋃ R1 On ∧ ran ⁡ R ∈ ⋃ R1 On → R ∈ ⋃ R1 On
10 3 9 impbid2 ⊢ Rel ⁡ R → R ∈ ⋃ R1 On ↔ dom ⁡ R ∈ ⋃ R1 On ∧ ran ⁡ R ∈ ⋃ R1 On