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 ( ∪ 𝐴 ⊆ ∩ 𝐴 ↔ ( 𝐴 = ∅ ∨ ∪ 𝐴 = ∩ 𝐴 ) )

Proof

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