Metamath Proof Explorer

Theorem eldmqs1cossres

Description: Elementhood in the domain quotient of the class of cosets by a restriction. (Contributed by Peter Mazsa, 4-May-2019)

Ref Expression
Assertion eldmqs1cossres ⊢ B ∈ V → B ∈ dom ⁡ ≀ R ↾ A / ≀ R ↾ A ↔ ∃ u ∈ A ∃ x ∈ u R B = x ≀ R ↾ A

Proof

Step Hyp Ref Expression
1 elqsg ⊢ B ∈ V → B ∈ dom ⁡ ≀ R ↾ A / ≀ R ↾ A ↔ ∃ x ∈ dom ⁡ ≀ R ↾ A B = x ≀ R ↾ A
2 df-rex ⊢ ∃ x ∈ dom ⁡ ≀ R ↾ A B = x ≀ R ↾ A ↔ ∃ x x ∈ dom ⁡ ≀ R ↾ A ∧ B = x ≀ R ↾ A
3 eldm1cossres2 ⊢ x ∈ V → x ∈ dom ⁡ ≀ R ↾ A ↔ ∃ u ∈ A x ∈ u R
4 3 elv ⊢ x ∈ dom ⁡ ≀ R ↾ A ↔ ∃ u ∈ A x ∈ u R
5 4 anbi1i ⊢ x ∈ dom ⁡ ≀ R ↾ A ∧ B = x ≀ R ↾ A ↔ ∃ u ∈ A x ∈ u R ∧ B = x ≀ R ↾ A
6 5 exbii ⊢ ∃ x x ∈ dom ⁡ ≀ R ↾ A ∧ B = x ≀ R ↾ A ↔ ∃ x ∃ u ∈ A x ∈ u R ∧ B = x ≀ R ↾ A
7 2 6 bitri ⊢ ∃ x ∈ dom ⁡ ≀ R ↾ A B = x ≀ R ↾ A ↔ ∃ x ∃ u ∈ A x ∈ u R ∧ B = x ≀ R ↾ A
8 1 7 syl6bb ⊢ B ∈ V → B ∈ dom ⁡ ≀ R ↾ A / ≀ R ↾ A ↔ ∃ x ∃ u ∈ A x ∈ u R ∧ B = x ≀ R ↾ A
9 df-rex ⊢ ∃ x ∈ u R B = x ≀ R ↾ A ↔ ∃ x x ∈ u R ∧ B = x ≀ R ↾ A
10 9 rexbii ⊢ ∃ u ∈ A ∃ x ∈ u R B = x ≀ R ↾ A ↔ ∃ u ∈ A ∃ x x ∈ u R ∧ B = x ≀ R ↾ A
11 rexcom4 ⊢ ∃ u ∈ A ∃ x x ∈ u R ∧ B = x ≀ R ↾ A ↔ ∃ x ∃ u ∈ A x ∈ u R ∧ B = x ≀ R ↾ A
12 r19.41v ⊢ ∃ u ∈ A x ∈ u R ∧ B = x ≀ R ↾ A ↔ ∃ u ∈ A x ∈ u R ∧ B = x ≀ R ↾ A
13 12 exbii ⊢ ∃ x ∃ u ∈ A x ∈ u R ∧ B = x ≀ R ↾ A ↔ ∃ x ∃ u ∈ A x ∈ u R ∧ B = x ≀ R ↾ A
14 11 13 bitri ⊢ ∃ u ∈ A ∃ x x ∈ u R ∧ B = x ≀ R ↾ A ↔ ∃ x ∃ u ∈ A x ∈ u R ∧ B = x ≀ R ↾ A
15 10 14 bitri ⊢ ∃ u ∈ A ∃ x ∈ u R B = x ≀ R ↾ A ↔ ∃ x ∃ u ∈ A x ∈ u R ∧ B = x ≀ R ↾ A
16 8 15 syl6bbr ⊢ B ∈ V → B ∈ dom ⁡ ≀ R ↾ A / ≀ R ↾ A ↔ ∃ u ∈ A ∃ x ∈ u R B = x ≀ R ↾ A