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

Metamath Proof Explorer

Theorem cossid

Description: Cosets by the identity relation are the identity relation. (Contributed by Peter Mazsa, 16-Jan-2019)

Ref Expression
Assertion cossid ≀ I = I

Proof

Step Hyp Ref Expression
1 equvinv ⊢ ( 𝑦 = 𝑧 ↔ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝑥 = 𝑧 ) )
2 ideqg ⊢ ( 𝑦 ∈ V → ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 ) )
3 2 elv ⊢ ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 )
4 ideqg ⊢ ( 𝑧 ∈ V → ( 𝑥 I 𝑧 ↔ 𝑥 = 𝑧 ) )
5 4 elv ⊢ ( 𝑥 I 𝑧 ↔ 𝑥 = 𝑧 )
6 3 5 anbi12i ⊢ ( ( 𝑥 I 𝑦 ∧ 𝑥 I 𝑧 ) ↔ ( 𝑥 = 𝑦 ∧ 𝑥 = 𝑧 ) )
7 6 exbii ⊢ ( ∃ 𝑥 ( 𝑥 I 𝑦 ∧ 𝑥 I 𝑧 ) ↔ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝑥 = 𝑧 ) )
8 1 7 bitr4i ⊢ ( 𝑦 = 𝑧 ↔ ∃ 𝑥 ( 𝑥 I 𝑦 ∧ 𝑥 I 𝑧 ) )
9 8 opabbii ⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑦 = 𝑧 } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ∃ 𝑥 ( 𝑥 I 𝑦 ∧ 𝑥 I 𝑧 ) }
10 df-id ⊢ I = { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝑦 = 𝑧 }
11 df-coss ⊢ ≀ I = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ∃ 𝑥 ( 𝑥 I 𝑦 ∧ 𝑥 I 𝑧 ) }
12 9 10 11 3eqtr4ri ⊢ ≀ I = I