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	⊢ ≀ ∅ = ∅