Metamath Proof Explorer

Theorem releldmqscoss

Description: Elementhood in the domain quotient of the class of cosets by a relation. (Contributed by Peter Mazsa, 23-Apr-2021)

Ref Expression
Assertion releldmqscoss ⊢ A ∈ V → Rel ⁡ R → A ∈ dom ⁡ ≀ R / ≀ R ↔ ∃ u ∈ dom ⁡ R ∃ x ∈ u R A = x ≀ R

Proof

Step Hyp Ref Expression
1 eldmqs1cossres ⊢ A ∈ V → A ∈ dom ⁡ ≀ R ↾ dom ⁡ R / ≀ R ↾ dom ⁡ R ↔ ∃ u ∈ dom ⁡ R ∃ x ∈ u R A = x ≀ R ↾ dom ⁡ R
2 1 adantr ⊢ A ∈ V ∧ Rel ⁡ R → A ∈ dom ⁡ ≀ R ↾ dom ⁡ R / ≀ R ↾ dom ⁡ R ↔ ∃ u ∈ dom ⁡ R ∃ x ∈ u R A = x ≀ R ↾ dom ⁡ R
3 resdm ⊢ Rel ⁡ R → R ↾ dom ⁡ R = R
4 3 cosseqd ⊢ Rel ⁡ R → ≀ R ↾ dom ⁡ R = ≀ R
5 4 dmqseqd ⊢ Rel ⁡ R → dom ⁡ ≀ R ↾ dom ⁡ R / ≀ R ↾ dom ⁡ R = dom ⁡ ≀ R / ≀ R
6 5 eleq2d ⊢ Rel ⁡ R → A ∈ dom ⁡ ≀ R ↾ dom ⁡ R / ≀ R ↾ dom ⁡ R ↔ A ∈ dom ⁡ ≀ R / ≀ R
7 6 adantl ⊢ A ∈ V ∧ Rel ⁡ R → A ∈ dom ⁡ ≀ R ↾ dom ⁡ R / ≀ R ↾ dom ⁡ R ↔ A ∈ dom ⁡ ≀ R / ≀ R
8 4 eceq2d ⊢ Rel ⁡ R → x ≀ R ↾ dom ⁡ R = x ≀ R
9 8 eqeq2d ⊢ Rel ⁡ R → A = x ≀ R ↾ dom ⁡ R ↔ A = x ≀ R
10 9 2rexbidv ⊢ Rel ⁡ R → ∃ u ∈ dom ⁡ R ∃ x ∈ u R A = x ≀ R ↾ dom ⁡ R ↔ ∃ u ∈ dom ⁡ R ∃ x ∈ u R A = x ≀ R
11 10 adantl ⊢ A ∈ V ∧ Rel ⁡ R → ∃ u ∈ dom ⁡ R ∃ x ∈ u R A = x ≀ R ↾ dom ⁡ R ↔ ∃ u ∈ dom ⁡ R ∃ x ∈ u R A = x ≀ R
12 2 7 11 3bitr3d ⊢ A ∈ V ∧ Rel ⁡ R → A ∈ dom ⁡ ≀ R / ≀ R ↔ ∃ u ∈ dom ⁡ R ∃ x ∈ u R A = x ≀ R
13 12 ex ⊢ A ∈ V → Rel ⁡ R → A ∈ dom ⁡ ≀ R / ≀ R ↔ ∃ u ∈ dom ⁡ R ∃ x ∈ u R A = x ≀ R