Theorem eceldmqsxrncnvepres2

Description: An ( R |X. ( ' E | A ) ) -coset in its domain quotient. In the pet span ( R |X. ( ' E | A ) ) , a block [ B ] lies in the domain quotient exactly when its representative B belongs to A and actually fires at least one arrow (has some x e. B and some y with B R y ). (Contributed by Peter Mazsa, 23-Nov-2025)

	Ref	Expression
Assertion	eceldmqsxrncnvepres2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) → ( [ 𝐵 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∈ ( dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) / ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) ↔ ( 𝐵 ∈ 𝐴 ∧ ∃ 𝑥 𝑥 ∈ 𝐵 ∧ ∃ 𝑦 𝐵 𝑅 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xrncnvepresex	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑋 ) → ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∈ V )
2		eceldmqs	⊢ ( ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∈ V → ( [ 𝐵 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∈ ( dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) / ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) ↔ 𝐵 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) )
3	1 2	syl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 ∈ 𝑋 ) → ( [ 𝐵 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∈ ( dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) / ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) ↔ 𝐵 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) )
4	3	3adant2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) → ( [ 𝐵 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∈ ( dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) / ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) ↔ 𝐵 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) )
5		eldmxrncnvepres2	⊢ ( 𝐵 ∈ 𝑊 → ( 𝐵 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↔ ( 𝐵 ∈ 𝐴 ∧ ∃ 𝑥 𝑥 ∈ 𝐵 ∧ ∃ 𝑦 𝐵 𝑅 𝑦 ) ) )
6	5	3ad2ant2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) → ( 𝐵 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↔ ( 𝐵 ∈ 𝐴 ∧ ∃ 𝑥 𝑥 ∈ 𝐵 ∧ ∃ 𝑦 𝐵 𝑅 𝑦 ) ) )
7	4 6	bitrd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) → ( [ 𝐵 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∈ ( dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) / ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) ↔ ( 𝐵 ∈ 𝐴 ∧ ∃ 𝑥 𝑥 ∈ 𝐵 ∧ ∃ 𝑦 𝐵 𝑅 𝑦 ) ) )