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

Metamath Proof Explorer

Theorem releldmqs

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

Ref Expression
Assertion releldmqs ( 𝐴 ∈ 𝑉 → ( Rel 𝑅 → ( 𝐴 ∈ ( dom 𝑅 / 𝑅 ) ↔ ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐴 = [ 𝑢 ] 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 resdm ⊢ ( Rel 𝑅 → ( 𝑅 ↾ dom 𝑅 ) = 𝑅 )
2 1 dmqseqd ⊢ ( Rel 𝑅 → ( dom ( 𝑅 ↾ dom 𝑅 ) / ( 𝑅 ↾ dom 𝑅 ) ) = ( dom 𝑅 / 𝑅 ) )
3 2 eleq2d ⊢ ( Rel 𝑅 → ( 𝐴 ∈ ( dom ( 𝑅 ↾ dom 𝑅 ) / ( 𝑅 ↾ dom 𝑅 ) ) ↔ 𝐴 ∈ ( dom 𝑅 / 𝑅 ) ) )
4 3 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Rel 𝑅 ) → ( 𝐴 ∈ ( dom ( 𝑅 ↾ dom 𝑅 ) / ( 𝑅 ↾ dom 𝑅 ) ) ↔ 𝐴 ∈ ( dom 𝑅 / 𝑅 ) ) )
5 eldmqsres2 ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ( dom ( 𝑅 ↾ dom 𝑅 ) / ( 𝑅 ↾ dom 𝑅 ) ) ↔ ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐴 = [ 𝑢 ] 𝑅 ) )
6 5 adantr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Rel 𝑅 ) → ( 𝐴 ∈ ( dom ( 𝑅 ↾ dom 𝑅 ) / ( 𝑅 ↾ dom 𝑅 ) ) ↔ ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐴 = [ 𝑢 ] 𝑅 ) )
7 4 6 bitr3d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ Rel 𝑅 ) → ( 𝐴 ∈ ( dom 𝑅 / 𝑅 ) ↔ ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐴 = [ 𝑢 ] 𝑅 ) )
8 7 ex ⊢ ( 𝐴 ∈ 𝑉 → ( Rel 𝑅 → ( 𝐴 ∈ ( dom 𝑅 / 𝑅 ) ↔ ∃ 𝑢 ∈ dom 𝑅 ∃ 𝑥 ∈ [ 𝑢 ] 𝑅 𝐴 = [ 𝑢 ] 𝑅 ) ) )