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 ⊢ A ∈ V ∧ B ∈ W ∧ R ∈ X → B R ⋉ E -1 ↾ A ∈ dom ⁡ R ⋉ E -1 ↾ A / R ⋉ E -1 ↾ A ↔ B ∈ A ∧ B ≠ ∅ ∧ B R ≠ ∅

Proof

Step Hyp Ref Expression
1 xrncnvepresex ⊢ A ∈ V ∧ R ∈ X → R ⋉ E -1 ↾ A ∈ V
2 eceldmqs ⊢ R ⋉ E -1 ↾ A ∈ V → B R ⋉ E -1 ↾ A ∈ dom ⁡ R ⋉ E -1 ↾ A / R ⋉ E -1 ↾ A ↔ B ∈ dom ⁡ R ⋉ E -1 ↾ A
3 1 2 syl ⊢ A ∈ V ∧ R ∈ X → B R ⋉ E -1 ↾ A ∈ dom ⁡ R ⋉ E -1 ↾ A / R ⋉ E -1 ↾ A ↔ B ∈ dom ⁡ R ⋉ E -1 ↾ A
4 3 3adant2 ⊢ A ∈ V ∧ B ∈ W ∧ R ∈ X → B R ⋉ E -1 ↾ A ∈ dom ⁡ R ⋉ E -1 ↾ A / R ⋉ E -1 ↾ A ↔ B ∈ dom ⁡ R ⋉ E -1 ↾ A
5 eldmxrncnvepres ⊢ B ∈ W → B ∈ dom ⁡ R ⋉ E -1 ↾ A ↔ B ∈ A ∧ B ≠ ∅ ∧ B R ≠ ∅
6 5 3ad2ant2 ⊢ A ∈ V ∧ B ∈ W ∧ R ∈ X → B ∈ dom ⁡ R ⋉ E -1 ↾ A ↔ B ∈ A ∧ B ≠ ∅ ∧ B R ≠ ∅
7 4 6 bitrd ⊢ A ∈ V ∧ B ∈ W ∧ R ∈ X → B R ⋉ E -1 ↾ A ∈ dom ⁡ R ⋉ E -1 ↾ A / R ⋉ E -1 ↾ A ↔ B ∈ A ∧ B ≠ ∅ ∧ B R ≠ ∅