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 ↾ 𝐴 ) ) ↔ ( 𝐵 ∈ 𝐴 ∧ ∃ 𝑥 𝑥 ∈ 𝐵 ∧ ∃ 𝑦 𝐵 𝑅 𝑦 ) ) )