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

Metamath Proof Explorer

Theorem 1cossres

Description: The class of cosets by a restriction. (Contributed by Peter Mazsa, 20-Apr-2019)

Ref Expression
Assertion 1cossres ≀ ( 𝑅 ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) }

Proof

Step Hyp Ref Expression
1 df-coss ⊢ ≀ ( 𝑅 ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑥 ∧ 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑦 ) }
2 df-rex ⊢ ( ∃ 𝑢 ∈ 𝐴 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) ↔ ∃ 𝑢 ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) ) )
3 anandi ⊢ ( ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) ) ↔ ( ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑥 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑦 ) ) )
4 brres ⊢ ( 𝑥 ∈ V → ( 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑥 ↔ ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑥 ) ) )
5 4 elv ⊢ ( 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑥 ↔ ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑥 ) )
6 brres ⊢ ( 𝑦 ∈ V → ( 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑦 ↔ ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑦 ) ) )
7 6 elv ⊢ ( 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑦 ↔ ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑦 ) )
8 5 7 anbi12i ⊢ ( ( 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑥 ∧ 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑦 ) ↔ ( ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑥 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑢 𝑅 𝑦 ) ) )
9 3 8 bitr4i ⊢ ( ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) ) ↔ ( 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑥 ∧ 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑦 ) )
10 9 exbii ⊢ ( ∃ 𝑢 ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) ) ↔ ∃ 𝑢 ( 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑥 ∧ 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑦 ) )
11 2 10 bitri ⊢ ( ∃ 𝑢 ∈ 𝐴 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) ↔ ∃ 𝑢 ( 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑥 ∧ 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑦 ) )
12 11 opabbii ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑥 ∧ 𝑢 ( 𝑅 ↾ 𝐴 ) 𝑦 ) }
13 1 12 eqtr4i ⊢ ≀ ( 𝑅 ↾ 𝐴 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) }