Theorem eceldmqsxrncnvepres

Description: An ( R |X. (`' _E |`A ) ) -coset in its domain quotient. (Contributed by Peter Mazsa, 23-Nov-2025)

	Ref	Expression
Assertion	eceldmqsxrncnvepres	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) → ( [ 𝐵 ] ( 𝑅 ⋉ ( ◡ 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		eldmxrncnvepres	⊢ ( 𝐵 ∈ 𝑊 → ( 𝐵 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ∧ [ 𝐵 ] 𝑅 ≠ ∅ ) ) )
6	5	3ad2ant2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) → ( 𝐵 ∈ dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ∧ [ 𝐵 ] 𝑅 ≠ ∅ ) ) )
7	4 6	bitrd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝑅 ∈ 𝑋 ) → ( [ 𝐵 ] ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ∈ ( dom ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) / ( 𝑅 ⋉ ( ◡ E ↾ 𝐴 ) ) ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ∧ [ 𝐵 ] 𝑅 ≠ ∅ ) ) )