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

Metamath Proof Explorer

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 ⊢ ( ∪ 𝐴 = ∩ 𝐴 ↔ ∃ 𝑥 𝐴 = { 𝑥 } )