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

Metamath Proof Explorer

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 ↾ 𝐴 ) ) ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 ≠ ∅ ∧ [ 𝐵 ] 𝑅 ≠ ∅ ) ) )