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

Metamath Proof Explorer

Theorem eldmxrncnvepres2

Description: Element of the domain of the range product with restricted converse epsilon relation. This identifies the domain of the pet span ( R |X. (`' _E |`A ) ) : a B belongs to the domain of the span exactly when B is in A and has at least one x e. B and y with B R y . (Contributed by Peter Mazsa, 23-Nov-2025)

Ref Expression
Assertion eldmxrncnvepres2 ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↔ ( 𝐵 ∈ 𝐴 ∧ ∃ 𝑥 𝑥 ∈ 𝐵 ∧ ∃ 𝑦 𝐵 𝑅 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 eldmres ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom ( 𝑅 ↾ 𝐴 ) ↔ ( 𝐵 ∈ 𝐴 ∧ ∃ 𝑦 𝐵 𝑅 𝑦 ) ) )
2 n0 ⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐵 )
3 2 a1i ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐵 ) )
4 1 3 anbi12d ⊢ ( 𝐵 ∈ 𝑉 → ( ( 𝐵 ∈ dom ( 𝑅 ↾ 𝐴 ) ∧ 𝐵 ≠ ∅ ) ↔ ( ( 𝐵 ∈ 𝐴 ∧ ∃ 𝑦 𝐵 𝑅 𝑦 ) ∧ ∃ 𝑥 𝑥 ∈ 𝐵 ) ) )
5 dmxrncnvepres ⊢ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) = ( dom ( 𝑅 ↾ 𝐴 ) ∖ { ∅ } )
6 5 eleq2i ⊢ ( 𝐵 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↔ 𝐵 ∈ ( dom ( 𝑅 ↾ 𝐴 ) ∖ { ∅ } ) )
7 eldifsn ⊢ ( 𝐵 ∈ ( dom ( 𝑅 ↾ 𝐴 ) ∖ { ∅ } ) ↔ ( 𝐵 ∈ dom ( 𝑅 ↾ 𝐴 ) ∧ 𝐵 ≠ ∅ ) )
8 6 7 bitri ⊢ ( 𝐵 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↔ ( 𝐵 ∈ dom ( 𝑅 ↾ 𝐴 ) ∧ 𝐵 ≠ ∅ ) )
9 3anan32 ⊢ ( ( 𝐵 ∈ 𝐴 ∧ ∃ 𝑥 𝑥 ∈ 𝐵 ∧ ∃ 𝑦 𝐵 𝑅 𝑦 ) ↔ ( ( 𝐵 ∈ 𝐴 ∧ ∃ 𝑦 𝐵 𝑅 𝑦 ) ∧ ∃ 𝑥 𝑥 ∈ 𝐵 ) )
10 4 8 9 3bitr4g ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐵 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↔ ( 𝐵 ∈ 𝐴 ∧ ∃ 𝑥 𝑥 ∈ 𝐵 ∧ ∃ 𝑦 𝐵 𝑅 𝑦 ) ) )