Theorem 0elsros

Description: A semiring of sets contains the empty set. (Contributed by Thierry Arnoux, 18-Jul-2020)

	Ref	Expression
Hypothesis	issros.1	⊢ 𝑁 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑠 ∧ ∃ 𝑧 ∈ 𝒫 𝑠 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) }
Assertion	0elsros	⊢ ( 𝑆 ∈ 𝑁 → ∅ ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		issros.1	⊢ 𝑁 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ∀ 𝑦 ∈ 𝑠 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑠 ∧ ∃ 𝑧 ∈ 𝒫 𝑠 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) }
2	1	issros	⊢ ( 𝑆 ∈ 𝑁 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ∅ ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑥 ∩ 𝑦 ) ∈ 𝑆 ∧ ∃ 𝑧 ∈ 𝒫 𝑆 ( 𝑧 ∈ Fin ∧ Disj 𝑡 ∈ 𝑧 𝑡 ∧ ( 𝑥 ∖ 𝑦 ) = ∪ 𝑧 ) ) ) )
3	2	simp2bi	⊢ ( 𝑆 ∈ 𝑁 → ∅ ∈ 𝑆 )