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