This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eldmxrncnvepres

Description: Element of the domain of the range product with restricted converse epsilon relation. (Contributed by Peter Mazsa, 23-Nov-2025)

Ref Expression
Assertion eldmxrncnvepres ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ∧ [ 𝐵 ] 𝑅 ≠ ∅ ) ) )

Proof

Step Hyp Ref Expression
1 eldmres3 ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom ( 𝑅 ↾ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ [ 𝐵 ] 𝑅 ≠ ∅ ) ) )
2 1 anbi1d ⊢ ( 𝐵 ∈ 𝑉 → ( ( 𝐵 ∈ dom ( 𝑅 ↾ 𝐴 ) ∧ 𝐵 ≠ ∅ ) ↔ ( ( 𝐵 ∈ 𝐴 ∧ [ 𝐵 ] 𝑅 ≠ ∅ ) ∧ 𝐵 ≠ ∅ ) ) )
3 dmxrncnvepres ⊢ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) = ( dom ( 𝑅 ↾ 𝐴 ) ∖ { ∅ } )
4 3 eleq2i ⊢ ( 𝐵 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↔ 𝐵 ∈ ( dom ( 𝑅 ↾ 𝐴 ) ∖ { ∅ } ) )
5 eldifsn ⊢ ( 𝐵 ∈ ( dom ( 𝑅 ↾ 𝐴 ) ∖ { ∅ } ) ↔ ( 𝐵 ∈ dom ( 𝑅 ↾ 𝐴 ) ∧ 𝐵 ≠ ∅ ) )
6 4 5 bitri ⊢ ( 𝐵 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↔ ( 𝐵 ∈ dom ( 𝑅 ↾ 𝐴 ) ∧ 𝐵 ≠ ∅ ) )
7 3anan32 ⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ∧ [ 𝐵 ] 𝑅 ≠ ∅ ) ↔ ( ( 𝐵 ∈ 𝐴 ∧ [ 𝐵 ] 𝑅 ≠ ∅ ) ∧ 𝐵 ≠ ∅ ) )
8 2 6 7 3bitr4g ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ∧ [ 𝐵 ] 𝑅 ≠ ∅ ) ) )