Theorem unissint 4953

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

Assertion

Ref	Expression
unissint	⊢ (∪ 𝐴 ⊆ ∩ 𝐴 ↔ (𝐴 = ∅ ∨ ∪ 𝐴 = ∩ 𝐴))

Proof of Theorem unissint

Step	Hyp	Ref	Expression
1		simpl 482	. . . . 5 ⊢ ((∪ 𝐴 ⊆ ∩ 𝐴 ∧ ¬ 𝐴 = ∅) → ∪ 𝐴 ⊆ ∩ 𝐴)
2		df-ne 2934	. . . . . . 7 ⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
3		intssuni 4951	. . . . . . 7 ⊢ (𝐴 ≠ ∅ → ∩ 𝐴 ⊆ ∪ 𝐴)
4	2, 3	sylbir 235	. . . . . 6 ⊢ (¬ 𝐴 = ∅ → ∩ 𝐴 ⊆ ∪ 𝐴)
5	4	adantl 481	. . . . 5 ⊢ ((∪ 𝐴 ⊆ ∩ 𝐴 ∧ ¬ 𝐴 = ∅) → ∩ 𝐴 ⊆ ∪ 𝐴)
6	1, 5	eqssd 3981	. . . 4 ⊢ ((∪ 𝐴 ⊆ ∩ 𝐴 ∧ ¬ 𝐴 = ∅) → ∪ 𝐴 = ∩ 𝐴)
7	6	ex 412	. . 3 ⊢ (∪ 𝐴 ⊆ ∩ 𝐴 → (¬ 𝐴 = ∅ → ∪ 𝐴 = ∩ 𝐴))
8	7	orrd 863	. 2 ⊢ (∪ 𝐴 ⊆ ∩ 𝐴 → (𝐴 = ∅ ∨ ∪ 𝐴 = ∩ 𝐴))
9		ssv 3988	. . . . 5 ⊢ ∪ 𝐴 ⊆ V
10		int0 4943	. . . . 5 ⊢ ∩ ∅ = V
11	9, 10	sseqtrri 4013	. . . 4 ⊢ ∪ 𝐴 ⊆ ∩ ∅
12		inteq 4930	. . . 4 ⊢ (𝐴 = ∅ → ∩ 𝐴 = ∩ ∅)
13	11, 12	sseqtrrid 4007	. . 3 ⊢ (𝐴 = ∅ → ∪ 𝐴 ⊆ ∩ 𝐴)
14		eqimss 4022	. . 3 ⊢ (∪ 𝐴 = ∩ 𝐴 → ∪ 𝐴 ⊆ ∩ 𝐴)
15	13, 14	jaoi 857	. 2 ⊢ ((𝐴 = ∅ ∨ ∪ 𝐴 = ∩ 𝐴) → ∪ 𝐴 ⊆ ∩ 𝐴)
16	8, 15	impbii 209	1 ⊢ (∪ 𝐴 ⊆ ∩ 𝐴 ↔ (𝐴 = ∅ ∨ ∪ 𝐴 = ∩ 𝐴))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540   ≠ wne 2933  Vcvv 3464   ⊆ wss 3931  ∅c0 4313  ∪ cuni 4888  ∩ cint 4927

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-ral 3053  df-rex 3062  df-v 3466  df-dif 3934  df-ss 3948  df-nul 4314  df-uni 4889  df-int 4928

This theorem is referenced by: (None)