Metamath Proof Explorer

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

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 eldmxrncnvepres2 ⊢ B ∈ W → B ∈ dom ⁡ R ⋉ E -1 ↾ A ↔ B ∈ A ∧ ∃ x x ∈ B ∧ ∃ y B R y
6 5 3ad2ant2 ⊢ A ∈ V ∧ B ∈ W ∧ R ∈ X → B ∈ dom ⁡ R ⋉ E -1 ↾ A ↔ B ∈ A ∧ ∃ x x ∈ B ∧ ∃ y B R y
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 ∧ ∃ x x ∈ B ∧ ∃ y B R y