Description: Sufficient condition for a range Cartesian product with restricted converse epsilon to be a set. (Contributed by Peter Mazsa, 16-Dec-2020) (Revised by Peter Mazsa, 23-Sep-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | xrncnvepresex | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∈ V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnvepresex | ⊢ ( 𝐴 ∈ 𝑉 → ( ◡ E ↾ 𝐴 ) ∈ V ) | |
2 | 1 | adantr | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( ◡ E ↾ 𝐴 ) ∈ V ) |
3 | xrnresex | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ∧ ( ◡ E ↾ 𝐴 ) ∈ V ) → ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∈ V ) | |
4 | 2 3 | mpd3an3 | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑊 ) → ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∈ V ) |