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

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 ( 𝐴 ∈ 𝑉 → ( Rel 𝑅 → ( 𝐴 ∈ ( dom ≀ 𝑅 / ≀ 𝑅 ) ↔ ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐴 = [ 𝑥 ] ≀ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 eldmqs1cossres ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ( dom ≀ ( 𝑅 ↾ dom 𝑅 ) / ≀ ( 𝑅 ↾ dom 𝑅 ) ) ↔ ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐴 = [ 𝑥 ] ≀ ( 𝑅 ↾ dom 𝑅 ) ) )
2 1 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Rel 𝑅 ) → ( 𝐴 ∈ ( dom ≀ ( 𝑅 ↾ dom 𝑅 ) / ≀ ( 𝑅 ↾ dom 𝑅 ) ) ↔ ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐴 = [ 𝑥 ] ≀ ( 𝑅 ↾ dom 𝑅 ) ) )
3 resdm ⊢ ( Rel 𝑅 → ( 𝑅 ↾ dom 𝑅 ) = 𝑅 )
4 3 cosseqd ⊢ ( Rel 𝑅 → ≀ ( 𝑅 ↾ dom 𝑅 ) = ≀ 𝑅 )
5 4 dmqseqd ⊢ ( Rel 𝑅 → ( dom ≀ ( 𝑅 ↾ dom 𝑅 ) / ≀ ( 𝑅 ↾ dom 𝑅 ) ) = ( dom ≀ 𝑅 / ≀ 𝑅 ) )
6 5 eleq2d ⊢ ( Rel 𝑅 → ( 𝐴 ∈ ( dom ≀ ( 𝑅 ↾ dom 𝑅 ) / ≀ ( 𝑅 ↾ dom 𝑅 ) ) ↔ 𝐴 ∈ ( dom ≀ 𝑅 / ≀ 𝑅 ) ) )
7 6 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Rel 𝑅 ) → ( 𝐴 ∈ ( dom ≀ ( 𝑅 ↾ dom 𝑅 ) / ≀ ( 𝑅 ↾ dom 𝑅 ) ) ↔ 𝐴 ∈ ( dom ≀ 𝑅 / ≀ 𝑅 ) ) )
8 4 eceq2d ⊢ ( Rel 𝑅 → [ 𝑥 ] ≀ ( 𝑅 ↾ dom 𝑅 ) = [ 𝑥 ] ≀ 𝑅 )
9 8 eqeq2d ⊢ ( Rel 𝑅 → ( 𝐴 = [ 𝑥 ] ≀ ( 𝑅 ↾ dom 𝑅 ) ↔ 𝐴 = [ 𝑥 ] ≀ 𝑅 ) )
10 9 2rexbidv ⊢ ( Rel 𝑅 → ( ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐴 = [ 𝑥 ] ≀ ( 𝑅 ↾ dom 𝑅 ) ↔ ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐴 = [ 𝑥 ] ≀ 𝑅 ) )
11 10 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Rel 𝑅 ) → ( ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐴 = [ 𝑥 ] ≀ ( 𝑅 ↾ dom 𝑅 ) ↔ ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐴 = [ 𝑥 ] ≀ 𝑅 ) )
12 2 7 11 3bitr3d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Rel 𝑅 ) → ( 𝐴 ∈ ( dom ≀ 𝑅 / ≀ 𝑅 ) ↔ ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐴 = [ 𝑥 ] ≀ 𝑅 ) )
13 12 ex ⊢ ( 𝐴 ∈ 𝑉 → ( Rel 𝑅 → ( 𝐴 ∈ ( dom ≀ 𝑅 / ≀ 𝑅 ) ↔ ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐴 = [ 𝑥 ] ≀ 𝑅 ) ) )