Theorem uniintsn

Description: Two ways to express " A is a singleton". See also en1 , en1b , card1 , and eusn . (Contributed by NM, 2-Aug-2010)

	Ref	Expression
Assertion	uniintsn	⊢ ( ∪ 𝐴 = ∩ 𝐴 ↔ ∃ 𝑥 𝐴 = { 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		vn0	⊢ V ≠ ∅
2		inteq	⊢ ( 𝐴 = ∅ → ∩ 𝐴 = ∩ ∅ )
3		int0	⊢ ∩ ∅ = V
4	2 3	eqtrdi	⊢ ( 𝐴 = ∅ → ∩ 𝐴 = V )
5	4	adantl	⊢ ( ( ∪ 𝐴 = ∩ 𝐴 ∧ 𝐴 = ∅ ) → ∩ 𝐴 = V )
6		unieq	⊢ ( 𝐴 = ∅ → ∪ 𝐴 = ∪ ∅ )
7		uni0	⊢ ∪ ∅ = ∅
8	6 7	eqtrdi	⊢ ( 𝐴 = ∅ → ∪ 𝐴 = ∅ )
9		eqeq1	⊢ ( ∪ 𝐴 = ∩ 𝐴 → ( ∪ 𝐴 = ∅ ↔ ∩ 𝐴 = ∅ ) )
10	8 9	imbitrid	⊢ ( ∪ 𝐴 = ∩ 𝐴 → ( 𝐴 = ∅ → ∩ 𝐴 = ∅ ) )
11	10	imp	⊢ ( ( ∪ 𝐴 = ∩ 𝐴 ∧ 𝐴 = ∅ ) → ∩ 𝐴 = ∅ )
12	5 11	eqtr3d	⊢ ( ( ∪ 𝐴 = ∩ 𝐴 ∧ 𝐴 = ∅ ) → V = ∅ )
13	12	ex	⊢ ( ∪ 𝐴 = ∩ 𝐴 → ( 𝐴 = ∅ → V = ∅ ) )
14	13	necon3d	⊢ ( ∪ 𝐴 = ∩ 𝐴 → ( V ≠ ∅ → 𝐴 ≠ ∅ ) )
15	1 14	mpi	⊢ ( ∪ 𝐴 = ∩ 𝐴 → 𝐴 ≠ ∅ )
16		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
17	15 16	sylib	⊢ ( ∪ 𝐴 = ∩ 𝐴 → ∃ 𝑥 𝑥 ∈ 𝐴 )
18		vex	⊢ 𝑥 ∈ V
19		vex	⊢ 𝑦 ∈ V
20	18 19	prss	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝐴 )
21		uniss	⊢ ( { 𝑥 , 𝑦 } ⊆ 𝐴 → ∪ { 𝑥 , 𝑦 } ⊆ ∪ 𝐴 )
22	21	adantl	⊢ ( ( ∪ 𝐴 = ∩ 𝐴 ∧ { 𝑥 , 𝑦 } ⊆ 𝐴 ) → ∪ { 𝑥 , 𝑦 } ⊆ ∪ 𝐴 )
23		simpl	⊢ ( ( ∪ 𝐴 = ∩ 𝐴 ∧ { 𝑥 , 𝑦 } ⊆ 𝐴 ) → ∪ 𝐴 = ∩ 𝐴 )
24	22 23	sseqtrd	⊢ ( ( ∪ 𝐴 = ∩ 𝐴 ∧ { 𝑥 , 𝑦 } ⊆ 𝐴 ) → ∪ { 𝑥 , 𝑦 } ⊆ ∩ 𝐴 )
25		intss	⊢ ( { 𝑥 , 𝑦 } ⊆ 𝐴 → ∩ 𝐴 ⊆ ∩ { 𝑥 , 𝑦 } )
26	25	adantl	⊢ ( ( ∪ 𝐴 = ∩ 𝐴 ∧ { 𝑥 , 𝑦 } ⊆ 𝐴 ) → ∩ 𝐴 ⊆ ∩ { 𝑥 , 𝑦 } )
27	24 26	sstrd	⊢ ( ( ∪ 𝐴 = ∩ 𝐴 ∧ { 𝑥 , 𝑦 } ⊆ 𝐴 ) → ∪ { 𝑥 , 𝑦 } ⊆ ∩ { 𝑥 , 𝑦 } )
28	18 19	unipr	⊢ ∪ { 𝑥 , 𝑦 } = ( 𝑥 ∪ 𝑦 )
29	18 19	intpr	⊢ ∩ { 𝑥 , 𝑦 } = ( 𝑥 ∩ 𝑦 )
30	27 28 29	3sstr3g	⊢ ( ( ∪ 𝐴 = ∩ 𝐴 ∧ { 𝑥 , 𝑦 } ⊆ 𝐴 ) → ( 𝑥 ∪ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) )
31		inss1	⊢ ( 𝑥 ∩ 𝑦 ) ⊆ 𝑥
32		ssun1	⊢ 𝑥 ⊆ ( 𝑥 ∪ 𝑦 )
33	31 32	sstri	⊢ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∪ 𝑦 )
34		eqss	⊢ ( ( 𝑥 ∪ 𝑦 ) = ( 𝑥 ∩ 𝑦 ) ↔ ( ( 𝑥 ∪ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) )
35		uneqin	⊢ ( ( 𝑥 ∪ 𝑦 ) = ( 𝑥 ∩ 𝑦 ) ↔ 𝑥 = 𝑦 )
36	34 35	bitr3i	⊢ ( ( ( 𝑥 ∪ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ↔ 𝑥 = 𝑦 )
37	30 33 36	sylanblc	⊢ ( ( ∪ 𝐴 = ∩ 𝐴 ∧ { 𝑥 , 𝑦 } ⊆ 𝐴 ) → 𝑥 = 𝑦 )
38	37	ex	⊢ ( ∪ 𝐴 = ∩ 𝐴 → ( { 𝑥 , 𝑦 } ⊆ 𝐴 → 𝑥 = 𝑦 ) )
39	20 38	biimtrid	⊢ ( ∪ 𝐴 = ∩ 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 = 𝑦 ) )
40	39	alrimivv	⊢ ( ∪ 𝐴 = ∩ 𝐴 → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 = 𝑦 ) )
41	17 40	jca	⊢ ( ∪ 𝐴 = ∩ 𝐴 → ( ∃ 𝑥 𝑥 ∈ 𝐴 ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 = 𝑦 ) ) )
42		euabsn	⊢ ( ∃! 𝑥 𝑥 ∈ 𝐴 ↔ ∃ 𝑥 { 𝑥 ∣ 𝑥 ∈ 𝐴 } = { 𝑥 } )
43		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
44	43	eu4	⊢ ( ∃! 𝑥 𝑥 ∈ 𝐴 ↔ ( ∃ 𝑥 𝑥 ∈ 𝐴 ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 = 𝑦 ) ) )
45		abid2	⊢ { 𝑥 ∣ 𝑥 ∈ 𝐴 } = 𝐴
46	45	eqeq1i	⊢ ( { 𝑥 ∣ 𝑥 ∈ 𝐴 } = { 𝑥 } ↔ 𝐴 = { 𝑥 } )
47	46	exbii	⊢ ( ∃ 𝑥 { 𝑥 ∣ 𝑥 ∈ 𝐴 } = { 𝑥 } ↔ ∃ 𝑥 𝐴 = { 𝑥 } )
48	42 44 47	3bitr3i	⊢ ( ( ∃ 𝑥 𝑥 ∈ 𝐴 ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑥 = 𝑦 ) ) ↔ ∃ 𝑥 𝐴 = { 𝑥 } )
49	41 48	sylib	⊢ ( ∪ 𝐴 = ∩ 𝐴 → ∃ 𝑥 𝐴 = { 𝑥 } )
50		unisnv	⊢ ∪ { 𝑥 } = 𝑥
51		unieq	⊢ ( 𝐴 = { 𝑥 } → ∪ 𝐴 = ∪ { 𝑥 } )
52		inteq	⊢ ( 𝐴 = { 𝑥 } → ∩ 𝐴 = ∩ { 𝑥 } )
53	18	intsn	⊢ ∩ { 𝑥 } = 𝑥
54	52 53	eqtrdi	⊢ ( 𝐴 = { 𝑥 } → ∩ 𝐴 = 𝑥 )
55	50 51 54	3eqtr4a	⊢ ( 𝐴 = { 𝑥 } → ∪ 𝐴 = ∩ 𝐴 )
56	55	exlimiv	⊢ ( ∃ 𝑥 𝐴 = { 𝑥 } → ∪ 𝐴 = ∩ 𝐴 )
57	49 56	impbii	⊢ ( ∪ 𝐴 = ∩ 𝐴 ↔ ∃ 𝑥 𝐴 = { 𝑥 } )