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

Metamath Proof Explorer

Theorem unissint

Description: If the union of a class is included in its intersection, the class is either the empty set or a singleton ( uniintsn ). (Contributed by NM, 30-Oct-2010) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion unissint ⊢ ⋃ A ⊆ ⋂ A ↔ A = ∅ ∨ ⋃ A = ⋂ A

Proof

Step Hyp Ref Expression
1 simpl ⊢ ⋃ A ⊆ ⋂ A ∧ ¬ A = ∅ → ⋃ A ⊆ ⋂ A
2 df-ne ⊢ A ≠ ∅ ↔ ¬ A = ∅
3 intssuni ⊢ A ≠ ∅ → ⋂ A ⊆ ⋃ A
4 2 3 sylbir ⊢ ¬ A = ∅ → ⋂ A ⊆ ⋃ A
5 4 adantl ⊢ ⋃ A ⊆ ⋂ A ∧ ¬ A = ∅ → ⋂ A ⊆ ⋃ A
6 1 5 eqssd ⊢ ⋃ A ⊆ ⋂ A ∧ ¬ A = ∅ → ⋃ A = ⋂ A
7 6 ex ⊢ ⋃ A ⊆ ⋂ A → ¬ A = ∅ → ⋃ A = ⋂ A
8 7 orrd ⊢ ⋃ A ⊆ ⋂ A → A = ∅ ∨ ⋃ A = ⋂ A
9 ssv ⊢ ⋃ A ⊆ V
10 int0 ⊢ ⋂ ∅ = V
11 9 10 sseqtrri ⊢ ⋃ A ⊆ ⋂ ∅
12 inteq ⊢ A = ∅ → ⋂ A = ⋂ ∅
13 11 12 sseqtrrid ⊢ A = ∅ → ⋃ A ⊆ ⋂ A
14 eqimss ⊢ ⋃ A = ⋂ A → ⋃ A ⊆ ⋂ A
15 13 14 jaoi ⊢ A = ∅ ∨ ⋃ A = ⋂ A → ⋃ A ⊆ ⋂ A
16 8 15 impbii ⊢ ⋃ A ⊆ ⋂ A ↔ A = ∅ ∨ ⋃ A = ⋂ A