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 ⊢ B ∈ V → B ∈ dom ⁡ R ⋉ E -1 ↾ A ↔ B ∈ A ∧ ∃ x x ∈ B ∧ ∃ y B R y

Proof

Step Hyp Ref Expression
1 eldmres ⊢ B ∈ V → B ∈ dom ⁡ R ↾ A ↔ B ∈ A ∧ ∃ y B R y
2 n0 ⊢ B ≠ ∅ ↔ ∃ x x ∈ B
3 2 a1i ⊢ B ∈ V → B ≠ ∅ ↔ ∃ x x ∈ B
4 1 3 anbi12d ⊢ B ∈ V → B ∈ dom ⁡ R ↾ A ∧ B ≠ ∅ ↔ B ∈ A ∧ ∃ y B R y ∧ ∃ x x ∈ B
5 dmxrncnvepres ⊢ dom ⁡ R ⋉ E -1 ↾ A = dom ⁡ R ↾ A ∖ ∅
6 5 eleq2i ⊢ B ∈ dom ⁡ R ⋉ E -1 ↾ A ↔ B ∈ dom ⁡ R ↾ A ∖ ∅
7 eldifsn ⊢ B ∈ dom ⁡ R ↾ A ∖ ∅ ↔ B ∈ dom ⁡ R ↾ A ∧ B ≠ ∅
8 6 7 bitri ⊢ B ∈ dom ⁡ R ⋉ E -1 ↾ A ↔ B ∈ dom ⁡ R ↾ A ∧ B ≠ ∅
9 3anan32 ⊢ B ∈ A ∧ ∃ x x ∈ B ∧ ∃ y B R y ↔ B ∈ A ∧ ∃ y B R y ∧ ∃ x x ∈ B
10 4 8 9 3bitr4g ⊢ B ∈ V → B ∈ dom ⁡ R ⋉ E -1 ↾ A ↔ B ∈ A ∧ ∃ x x ∈ B ∧ ∃ y B R y