Metamath Proof Explorer

Theorem uneqsn

Description: If a union of classes is equal to a singleton then at least one class is equal to the singleton while the other may be equal to the empty set. (Contributed by RP, 5-Jul-2021)

Ref Expression
Assertion uneqsn ⊢ A ∪ B = C ↔ A = C ∧ B = C ∨ A = C ∧ B = ∅ ∨ A = ∅ ∧ B = C

Proof

Step Hyp Ref Expression
1 eqss ⊢ A ∪ B = C ↔ A ∪ B ⊆ C ∧ C ⊆ A ∪ B
2 1 a1i ⊢ C ∈ V → A ∪ B = C ↔ A ∪ B ⊆ C ∧ C ⊆ A ∪ B
3 unss ⊢ A ⊆ C ∧ B ⊆ C ↔ A ∪ B ⊆ C
4 3 bicomi ⊢ A ∪ B ⊆ C ↔ A ⊆ C ∧ B ⊆ C
5 4 a1i ⊢ C ∈ V → A ∪ B ⊆ C ↔ A ⊆ C ∧ B ⊆ C
6 elun ⊢ C ∈ A ∪ B ↔ C ∈ A ∨ C ∈ B
7 snssg ⊢ C ∈ V → C ∈ A ↔ C ⊆ A
8 snssg ⊢ C ∈ V → C ∈ B ↔ C ⊆ B
9 7 8 orbi12d ⊢ C ∈ V → C ∈ A ∨ C ∈ B ↔ C ⊆ A ∨ C ⊆ B
10 6 9 syl5rbb ⊢ C ∈ V → C ⊆ A ∨ C ⊆ B ↔ C ∈ A ∪ B
11 snssg ⊢ C ∈ V → C ∈ A ∪ B ↔ C ⊆ A ∪ B
12 10 11 bitr2d ⊢ C ∈ V → C ⊆ A ∪ B ↔ C ⊆ A ∨ C ⊆ B
13 5 12 anbi12d ⊢ C ∈ V → A ∪ B ⊆ C ∧ C ⊆ A ∪ B ↔ A ⊆ C ∧ B ⊆ C ∧ C ⊆ A ∨ C ⊆ B
14 or3or ⊢ C ⊆ A ∨ C ⊆ B ↔ C ⊆ A ∧ C ⊆ B ∨ C ⊆ A ∧ ¬ C ⊆ B ∨ ¬ C ⊆ A ∧ C ⊆ B
15 14 anbi2i ⊢ A ⊆ C ∧ B ⊆ C ∧ C ⊆ A ∨ C ⊆ B ↔ A ⊆ C ∧ B ⊆ C ∧ C ⊆ A ∧ C ⊆ B ∨ C ⊆ A ∧ ¬ C ⊆ B ∨ ¬ C ⊆ A ∧ C ⊆ B
16 andi3or ⊢ A ⊆ C ∧ B ⊆ C ∧ C ⊆ A ∧ C ⊆ B ∨ C ⊆ A ∧ ¬ C ⊆ B ∨ ¬ C ⊆ A ∧ C ⊆ B ↔ A ⊆ C ∧ B ⊆ C ∧ C ⊆ A ∧ C ⊆ B ∨ A ⊆ C ∧ B ⊆ C ∧ C ⊆ A ∧ ¬ C ⊆ B ∨ A ⊆ C ∧ B ⊆ C ∧ ¬ C ⊆ A ∧ C ⊆ B
17 15 16 bitri ⊢ A ⊆ C ∧ B ⊆ C ∧ C ⊆ A ∨ C ⊆ B ↔ A ⊆ C ∧ B ⊆ C ∧ C ⊆ A ∧ C ⊆ B ∨ A ⊆ C ∧ B ⊆ C ∧ C ⊆ A ∧ ¬ C ⊆ B ∨ A ⊆ C ∧ B ⊆ C ∧ ¬ C ⊆ A ∧ C ⊆ B
18 an4 ⊢ A ⊆ C ∧ B ⊆ C ∧ C ⊆ A ∧ C ⊆ B ↔ A ⊆ C ∧ C ⊆ A ∧ B ⊆ C ∧ C ⊆ B
19 eqss ⊢ A = C ↔ A ⊆ C ∧ C ⊆ A
20 eqss ⊢ B = C ↔ B ⊆ C ∧ C ⊆ B
21 19 20 anbi12i ⊢ A = C ∧ B = C ↔ A ⊆ C ∧ C ⊆ A ∧ B ⊆ C ∧ C ⊆ B
22 21 bicomi ⊢ A ⊆ C ∧ C ⊆ A ∧ B ⊆ C ∧ C ⊆ B ↔ A = C ∧ B = C
23 18 22 bitri ⊢ A ⊆ C ∧ B ⊆ C ∧ C ⊆ A ∧ C ⊆ B ↔ A = C ∧ B = C
24 23 a1i ⊢ C ∈ V → A ⊆ C ∧ B ⊆ C ∧ C ⊆ A ∧ C ⊆ B ↔ A = C ∧ B = C
25 an4 ⊢ A ⊆ C ∧ B ⊆ C ∧ C ⊆ A ∧ ¬ C ⊆ B ↔ A ⊆ C ∧ C ⊆ A ∧ B ⊆ C ∧ ¬ C ⊆ B
26 19 bicomi ⊢ A ⊆ C ∧ C ⊆ A ↔ A = C
27 26 a1i ⊢ C ∈ V → A ⊆ C ∧ C ⊆ A ↔ A = C
28 sssn ⊢ B ⊆ C ↔ B = ∅ ∨ B = C
29 28 a1i ⊢ C ∈ V → B ⊆ C ↔ B = ∅ ∨ B = C
30 29 anbi1d ⊢ C ∈ V → B ⊆ C ∧ ¬ C ⊆ B ↔ B = ∅ ∨ B = C ∧ ¬ C ⊆ B
31 andir ⊢ B = ∅ ∨ B = C ∧ ¬ C ⊆ B ↔ B = ∅ ∧ ¬ C ⊆ B ∨ B = C ∧ ¬ C ⊆ B
32 n0i ⊢ C ∈ B → ¬ B = ∅
33 8 32 syl6bir ⊢ C ∈ V → C ⊆ B → ¬ B = ∅
34 33 con2d ⊢ C ∈ V → B = ∅ → ¬ C ⊆ B
35 34 pm4.71d ⊢ C ∈ V → B = ∅ ↔ B = ∅ ∧ ¬ C ⊆ B
36 eqimss2 ⊢ B = C → C ⊆ B
37 iman ⊢ B = C → C ⊆ B ↔ ¬ B = C ∧ ¬ C ⊆ B
38 36 37 mpbi ⊢ ¬ B = C ∧ ¬ C ⊆ B
39 38 biorfi ⊢ B = ∅ ∧ ¬ C ⊆ B ↔ B = ∅ ∧ ¬ C ⊆ B ∨ B = C ∧ ¬ C ⊆ B
40 35 39 bitr2di ⊢ C ∈ V → B = ∅ ∧ ¬ C ⊆ B ∨ B = C ∧ ¬ C ⊆ B ↔ B = ∅
41 31 40 syl5bb ⊢ C ∈ V → B = ∅ ∨ B = C ∧ ¬ C ⊆ B ↔ B = ∅
42 30 41 bitrd ⊢ C ∈ V → B ⊆ C ∧ ¬ C ⊆ B ↔ B = ∅
43 27 42 anbi12d ⊢ C ∈ V → A ⊆ C ∧ C ⊆ A ∧ B ⊆ C ∧ ¬ C ⊆ B ↔ A = C ∧ B = ∅
44 25 43 syl5bb ⊢ C ∈ V → A ⊆ C ∧ B ⊆ C ∧ C ⊆ A ∧ ¬ C ⊆ B ↔ A = C ∧ B = ∅
45 an4 ⊢ A ⊆ C ∧ B ⊆ C ∧ ¬ C ⊆ A ∧ C ⊆ B ↔ A ⊆ C ∧ ¬ C ⊆ A ∧ B ⊆ C ∧ C ⊆ B
46 sssn ⊢ A ⊆ C ↔ A = ∅ ∨ A = C
47 46 a1i ⊢ C ∈ V → A ⊆ C ↔ A = ∅ ∨ A = C
48 47 anbi1d ⊢ C ∈ V → A ⊆ C ∧ ¬ C ⊆ A ↔ A = ∅ ∨ A = C ∧ ¬ C ⊆ A
49 andir ⊢ A = ∅ ∨ A = C ∧ ¬ C ⊆ A ↔ A = ∅ ∧ ¬ C ⊆ A ∨ A = C ∧ ¬ C ⊆ A
50 n0i ⊢ C ∈ A → ¬ A = ∅
51 7 50 syl6bir ⊢ C ∈ V → C ⊆ A → ¬ A = ∅
52 51 con2d ⊢ C ∈ V → A = ∅ → ¬ C ⊆ A
53 52 pm4.71d ⊢ C ∈ V → A = ∅ ↔ A = ∅ ∧ ¬ C ⊆ A
54 eqimss2 ⊢ A = C → C ⊆ A
55 iman ⊢ A = C → C ⊆ A ↔ ¬ A = C ∧ ¬ C ⊆ A
56 54 55 mpbi ⊢ ¬ A = C ∧ ¬ C ⊆ A
57 56 biorfi ⊢ A = ∅ ∧ ¬ C ⊆ A ↔ A = ∅ ∧ ¬ C ⊆ A ∨ A = C ∧ ¬ C ⊆ A
58 53 57 bitr2di ⊢ C ∈ V → A = ∅ ∧ ¬ C ⊆ A ∨ A = C ∧ ¬ C ⊆ A ↔ A = ∅
59 49 58 syl5bb ⊢ C ∈ V → A = ∅ ∨ A = C ∧ ¬ C ⊆ A ↔ A = ∅
60 48 59 bitrd ⊢ C ∈ V → A ⊆ C ∧ ¬ C ⊆ A ↔ A = ∅
61 20 bicomi ⊢ B ⊆ C ∧ C ⊆ B ↔ B = C
62 61 a1i ⊢ C ∈ V → B ⊆ C ∧ C ⊆ B ↔ B = C
63 60 62 anbi12d ⊢ C ∈ V → A ⊆ C ∧ ¬ C ⊆ A ∧ B ⊆ C ∧ C ⊆ B ↔ A = ∅ ∧ B = C
64 45 63 syl5bb ⊢ C ∈ V → A ⊆ C ∧ B ⊆ C ∧ ¬ C ⊆ A ∧ C ⊆ B ↔ A = ∅ ∧ B = C
65 24 44 64 3orbi123d ⊢ C ∈ V → A ⊆ C ∧ B ⊆ C ∧ C ⊆ A ∧ C ⊆ B ∨ A ⊆ C ∧ B ⊆ C ∧ C ⊆ A ∧ ¬ C ⊆ B ∨ A ⊆ C ∧ B ⊆ C ∧ ¬ C ⊆ A ∧ C ⊆ B ↔ A = C ∧ B = C ∨ A = C ∧ B = ∅ ∨ A = ∅ ∧ B = C
66 17 65 syl5bb ⊢ C ∈ V → A ⊆ C ∧ B ⊆ C ∧ C ⊆ A ∨ C ⊆ B ↔ A = C ∧ B = C ∨ A = C ∧ B = ∅ ∨ A = ∅ ∧ B = C
67 2 13 66 3bitrd ⊢ C ∈ V → A ∪ B = C ↔ A = C ∧ B = C ∨ A = C ∧ B = ∅ ∨ A = ∅ ∧ B = C
68 snprc ⊢ ¬ C ∈ V ↔ C = ∅
69 68 biimpi ⊢ ¬ C ∈ V → C = ∅
70 69 eqeq2d ⊢ ¬ C ∈ V → A ∪ B = C ↔ A ∪ B = ∅
71 pm4.25 ⊢ A = ∅ ∧ B = ∅ ↔ A = ∅ ∧ B = ∅ ∨ A = ∅ ∧ B = ∅
72 71 orbi1i ⊢ A = ∅ ∧ B = ∅ ∨ A = ∅ ∧ B = ∅ ↔ A = ∅ ∧ B = ∅ ∨ A = ∅ ∧ B = ∅ ∨ A = ∅ ∧ B = ∅
73 71 72 bitri ⊢ A = ∅ ∧ B = ∅ ↔ A = ∅ ∧ B = ∅ ∨ A = ∅ ∧ B = ∅ ∨ A = ∅ ∧ B = ∅
74 69 eqeq2d ⊢ ¬ C ∈ V → A = C ↔ A = ∅
75 69 eqeq2d ⊢ ¬ C ∈ V → B = C ↔ B = ∅
76 74 75 anbi12d ⊢ ¬ C ∈ V → A = C ∧ B = C ↔ A = ∅ ∧ B = ∅
77 74 anbi1d ⊢ ¬ C ∈ V → A = C ∧ B = ∅ ↔ A = ∅ ∧ B = ∅
78 76 77 orbi12d ⊢ ¬ C ∈ V → A = C ∧ B = C ∨ A = C ∧ B = ∅ ↔ A = ∅ ∧ B = ∅ ∨ A = ∅ ∧ B = ∅
79 75 anbi2d ⊢ ¬ C ∈ V → A = ∅ ∧ B = C ↔ A = ∅ ∧ B = ∅
80 78 79 orbi12d ⊢ ¬ C ∈ V → A = C ∧ B = C ∨ A = C ∧ B = ∅ ∨ A = ∅ ∧ B = C ↔ A = ∅ ∧ B = ∅ ∨ A = ∅ ∧ B = ∅ ∨ A = ∅ ∧ B = ∅
81 73 80 bitr4id ⊢ ¬ C ∈ V → A = ∅ ∧ B = ∅ ↔ A = C ∧ B = C ∨ A = C ∧ B = ∅ ∨ A = ∅ ∧ B = C
82 un00 ⊢ A = ∅ ∧ B = ∅ ↔ A ∪ B = ∅
83 82 bicomi ⊢ A ∪ B = ∅ ↔ A = ∅ ∧ B = ∅
84 df-3or ⊢ A = C ∧ B = C ∨ A = C ∧ B = ∅ ∨ A = ∅ ∧ B = C ↔ A = C ∧ B = C ∨ A = C ∧ B = ∅ ∨ A = ∅ ∧ B = C
85 81 83 84 3bitr4g ⊢ ¬ C ∈ V → A ∪ B = ∅ ↔ A = C ∧ B = C ∨ A = C ∧ B = ∅ ∨ A = ∅ ∧ B = C
86 70 85 bitrd ⊢ ¬ C ∈ V → A ∪ B = C ↔ A = C ∧ B = C ∨ A = C ∧ B = ∅ ∨ A = ∅ ∧ B = C
87 67 86 pm2.61i ⊢ A ∪ B = C ↔ A = C ∧ B = C ∨ A = C ∧ B = ∅ ∨ A = ∅ ∧ B = C