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

Metamath Proof Explorer

Theorem coss0

Description: Cosets by the empty set are the empty set. (Contributed by Peter Mazsa, 22-Oct-2019)

Ref Expression
Assertion coss0 ≀ ∅ = ∅

Proof

Step Hyp Ref Expression
1 dfcoss2 ⊢ ≀ ∅ = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ∃ 𝑥 ( 𝑦 ∈ [ 𝑥 ] ∅ ∧ 𝑧 ∈ [ 𝑥 ] ∅ ) }
2 ec0 ⊢ [ 𝑥 ] ∅ = ∅
3 2 eleq2i ⊢ ( 𝑦 ∈ [ 𝑥 ] ∅ ↔ 𝑦 ∈ ∅ )
4 2 eleq2i ⊢ ( 𝑧 ∈ [ 𝑥 ] ∅ ↔ 𝑧 ∈ ∅ )
5 3 4 anbi12i ⊢ ( ( 𝑦 ∈ [ 𝑥 ] ∅ ∧ 𝑧 ∈ [ 𝑥 ] ∅ ) ↔ ( 𝑦 ∈ ∅ ∧ 𝑧 ∈ ∅ ) )
6 5 exbii ⊢ ( ∃ 𝑥 ( 𝑦 ∈ [ 𝑥 ] ∅ ∧ 𝑧 ∈ [ 𝑥 ] ∅ ) ↔ ∃ 𝑥 ( 𝑦 ∈ ∅ ∧ 𝑧 ∈ ∅ ) )
7 19.9v ⊢ ( ∃ 𝑥 ( 𝑦 ∈ ∅ ∧ 𝑧 ∈ ∅ ) ↔ ( 𝑦 ∈ ∅ ∧ 𝑧 ∈ ∅ ) )
8 6 7 bitri ⊢ ( ∃ 𝑥 ( 𝑦 ∈ [ 𝑥 ] ∅ ∧ 𝑧 ∈ [ 𝑥 ] ∅ ) ↔ ( 𝑦 ∈ ∅ ∧ 𝑧 ∈ ∅ ) )
9 8 opabbii ⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ∃ 𝑥 ( 𝑦 ∈ [ 𝑥 ] ∅ ∧ 𝑧 ∈ [ 𝑥 ] ∅ ) } = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ∅ ∧ 𝑧 ∈ ∅ ) }
10 prnzg ⊢ ( 𝑦 ∈ V → { 𝑦 , 𝑧 } ≠ ∅ )
11 10 elv ⊢ { 𝑦 , 𝑧 } ≠ ∅
12 ss0b ⊢ ( { 𝑦 , 𝑧 } ⊆ ∅ ↔ { 𝑦 , 𝑧 } = ∅ )
13 11 12 nemtbir ⊢ ¬ { 𝑦 , 𝑧 } ⊆ ∅
14 prssg ⊢ ( ( 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( ( 𝑦 ∈ ∅ ∧ 𝑧 ∈ ∅ ) ↔ { 𝑦 , 𝑧 } ⊆ ∅ ) )
15 14 el2v ⊢ ( ( 𝑦 ∈ ∅ ∧ 𝑧 ∈ ∅ ) ↔ { 𝑦 , 𝑧 } ⊆ ∅ )
16 13 15 mtbir ⊢ ¬ ( 𝑦 ∈ ∅ ∧ 𝑧 ∈ ∅ )
17 16 opabf ⊢ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑦 ∈ ∅ ∧ 𝑧 ∈ ∅ ) } = ∅
18 1 9 17 3eqtri ⊢ ≀ ∅ = ∅