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 u. B ) = { C } <-> ( ( A = { C } /\ B = { C } ) \/ ( A = { C } /\ B = (/) ) \/ ( A = (/) /\ B = { C } ) ) )

Proof

Step Hyp Ref Expression
1 eqss 
 |-  ( ( A u. B ) = { C } <-> ( ( A u. B ) C_ { C } /\ { C } C_ ( A u. B ) ) )
2 1 a1i 
 |-  ( C e. _V -> ( ( A u. B ) = { C } <-> ( ( A u. B ) C_ { C } /\ { C } C_ ( A u. B ) ) ) )
3 unss 
 |-  ( ( A C_ { C } /\ B C_ { C } ) <-> ( A u. B ) C_ { C } )
4 3 bicomi 
 |-  ( ( A u. B ) C_ { C } <-> ( A C_ { C } /\ B C_ { C } ) )
5 4 a1i 
 |-  ( C e. _V -> ( ( A u. B ) C_ { C } <-> ( A C_ { C } /\ B C_ { C } ) ) )
6 elun 
 |-  ( C e. ( A u. B ) <-> ( C e. A \/ C e. B ) )
7 snssg 
 |-  ( C e. _V -> ( C e. A <-> { C } C_ A ) )
8 snssg 
 |-  ( C e. _V -> ( C e. B <-> { C } C_ B ) )
9 7 8 orbi12d 
 |-  ( C e. _V -> ( ( C e. A \/ C e. B ) <-> ( { C } C_ A \/ { C } C_ B ) ) )
10 6 9 bitr2id 
 |-  ( C e. _V -> ( ( { C } C_ A \/ { C } C_ B ) <-> C e. ( A u. B ) ) )
11 snssg 
 |-  ( C e. _V -> ( C e. ( A u. B ) <-> { C } C_ ( A u. B ) ) )
12 10 11 bitr2d 
 |-  ( C e. _V -> ( { C } C_ ( A u. B ) <-> ( { C } C_ A \/ { C } C_ B ) ) )
13 5 12 anbi12d 
 |-  ( C e. _V -> ( ( ( A u. B ) C_ { C } /\ { C } C_ ( A u. B ) ) <-> ( ( A C_ { C } /\ B C_ { C } ) /\ ( { C } C_ A \/ { C } C_ B ) ) ) )
14 or3or 
 |-  ( ( { C } C_ A \/ { C } C_ B ) <-> ( ( { C } C_ A /\ { C } C_ B ) \/ ( { C } C_ A /\ -. { C } C_ B ) \/ ( -. { C } C_ A /\ { C } C_ B ) ) )
15 14 anbi2i 
 |-  ( ( ( A C_ { C } /\ B C_ { C } ) /\ ( { C } C_ A \/ { C } C_ B ) ) <-> ( ( A C_ { C } /\ B C_ { C } ) /\ ( ( { C } C_ A /\ { C } C_ B ) \/ ( { C } C_ A /\ -. { C } C_ B ) \/ ( -. { C } C_ A /\ { C } C_ B ) ) ) )
16 andi3or 
 |-  ( ( ( A C_ { C } /\ B C_ { C } ) /\ ( ( { C } C_ A /\ { C } C_ B ) \/ ( { C } C_ A /\ -. { C } C_ B ) \/ ( -. { C } C_ A /\ { C } C_ B ) ) ) <-> ( ( ( A C_ { C } /\ B C_ { C } ) /\ ( { C } C_ A /\ { C } C_ B ) ) \/ ( ( A C_ { C } /\ B C_ { C } ) /\ ( { C } C_ A /\ -. { C } C_ B ) ) \/ ( ( A C_ { C } /\ B C_ { C } ) /\ ( -. { C } C_ A /\ { C } C_ B ) ) ) )
17 15 16 bitri 
 |-  ( ( ( A C_ { C } /\ B C_ { C } ) /\ ( { C } C_ A \/ { C } C_ B ) ) <-> ( ( ( A C_ { C } /\ B C_ { C } ) /\ ( { C } C_ A /\ { C } C_ B ) ) \/ ( ( A C_ { C } /\ B C_ { C } ) /\ ( { C } C_ A /\ -. { C } C_ B ) ) \/ ( ( A C_ { C } /\ B C_ { C } ) /\ ( -. { C } C_ A /\ { C } C_ B ) ) ) )
18 an4 
 |-  ( ( ( A C_ { C } /\ B C_ { C } ) /\ ( { C } C_ A /\ { C } C_ B ) ) <-> ( ( A C_ { C } /\ { C } C_ A ) /\ ( B C_ { C } /\ { C } C_ B ) ) )
19 eqss 
 |-  ( A = { C } <-> ( A C_ { C } /\ { C } C_ A ) )
20 eqss 
 |-  ( B = { C } <-> ( B C_ { C } /\ { C } C_ B ) )
21 19 20 anbi12i 
 |-  ( ( A = { C } /\ B = { C } ) <-> ( ( A C_ { C } /\ { C } C_ A ) /\ ( B C_ { C } /\ { C } C_ B ) ) )
22 21 bicomi 
 |-  ( ( ( A C_ { C } /\ { C } C_ A ) /\ ( B C_ { C } /\ { C } C_ B ) ) <-> ( A = { C } /\ B = { C } ) )
23 18 22 bitri 
 |-  ( ( ( A C_ { C } /\ B C_ { C } ) /\ ( { C } C_ A /\ { C } C_ B ) ) <-> ( A = { C } /\ B = { C } ) )
24 23 a1i 
 |-  ( C e. _V -> ( ( ( A C_ { C } /\ B C_ { C } ) /\ ( { C } C_ A /\ { C } C_ B ) ) <-> ( A = { C } /\ B = { C } ) ) )
25 an4 
 |-  ( ( ( A C_ { C } /\ B C_ { C } ) /\ ( { C } C_ A /\ -. { C } C_ B ) ) <-> ( ( A C_ { C } /\ { C } C_ A ) /\ ( B C_ { C } /\ -. { C } C_ B ) ) )
26 19 bicomi 
 |-  ( ( A C_ { C } /\ { C } C_ A ) <-> A = { C } )
27 26 a1i 
 |-  ( C e. _V -> ( ( A C_ { C } /\ { C } C_ A ) <-> A = { C } ) )
28 sssn 
 |-  ( B C_ { C } <-> ( B = (/) \/ B = { C } ) )
29 28 a1i 
 |-  ( C e. _V -> ( B C_ { C } <-> ( B = (/) \/ B = { C } ) ) )
30 29 anbi1d 
 |-  ( C e. _V -> ( ( B C_ { C } /\ -. { C } C_ B ) <-> ( ( B = (/) \/ B = { C } ) /\ -. { C } C_ B ) ) )
31 andir 
 |-  ( ( ( B = (/) \/ B = { C } ) /\ -. { C } C_ B ) <-> ( ( B = (/) /\ -. { C } C_ B ) \/ ( B = { C } /\ -. { C } C_ B ) ) )
32 n0i 
 |-  ( C e. B -> -. B = (/) )
33 8 32 biimtrrdi 
 |-  ( C e. _V -> ( { C } C_ B -> -. B = (/) ) )
34 33 con2d 
 |-  ( C e. _V -> ( B = (/) -> -. { C } C_ B ) )
35 34 pm4.71d 
 |-  ( C e. _V -> ( B = (/) <-> ( B = (/) /\ -. { C } C_ B ) ) )
36 eqimss2 
 |-  ( B = { C } -> { C } C_ B )
37 iman 
 |-  ( ( B = { C } -> { C } C_ B ) <-> -. ( B = { C } /\ -. { C } C_ B ) )
38 36 37 mpbi 
 |-  -. ( B = { C } /\ -. { C } C_ B )
39 38 biorfri 
 |-  ( ( B = (/) /\ -. { C } C_ B ) <-> ( ( B = (/) /\ -. { C } C_ B ) \/ ( B = { C } /\ -. { C } C_ B ) ) )
40 35 39 bitr2di 
 |-  ( C e. _V -> ( ( ( B = (/) /\ -. { C } C_ B ) \/ ( B = { C } /\ -. { C } C_ B ) ) <-> B = (/) ) )
41 31 40 bitrid 
 |-  ( C e. _V -> ( ( ( B = (/) \/ B = { C } ) /\ -. { C } C_ B ) <-> B = (/) ) )
42 30 41 bitrd 
 |-  ( C e. _V -> ( ( B C_ { C } /\ -. { C } C_ B ) <-> B = (/) ) )
43 27 42 anbi12d 
 |-  ( C e. _V -> ( ( ( A C_ { C } /\ { C } C_ A ) /\ ( B C_ { C } /\ -. { C } C_ B ) ) <-> ( A = { C } /\ B = (/) ) ) )
44 25 43 bitrid 
 |-  ( C e. _V -> ( ( ( A C_ { C } /\ B C_ { C } ) /\ ( { C } C_ A /\ -. { C } C_ B ) ) <-> ( A = { C } /\ B = (/) ) ) )
45 an4 
 |-  ( ( ( A C_ { C } /\ B C_ { C } ) /\ ( -. { C } C_ A /\ { C } C_ B ) ) <-> ( ( A C_ { C } /\ -. { C } C_ A ) /\ ( B C_ { C } /\ { C } C_ B ) ) )
46 sssn 
 |-  ( A C_ { C } <-> ( A = (/) \/ A = { C } ) )
47 46 a1i 
 |-  ( C e. _V -> ( A C_ { C } <-> ( A = (/) \/ A = { C } ) ) )
48 47 anbi1d 
 |-  ( C e. _V -> ( ( A C_ { C } /\ -. { C } C_ A ) <-> ( ( A = (/) \/ A = { C } ) /\ -. { C } C_ A ) ) )
49 andir 
 |-  ( ( ( A = (/) \/ A = { C } ) /\ -. { C } C_ A ) <-> ( ( A = (/) /\ -. { C } C_ A ) \/ ( A = { C } /\ -. { C } C_ A ) ) )
50 n0i 
 |-  ( C e. A -> -. A = (/) )
51 7 50 biimtrrdi 
 |-  ( C e. _V -> ( { C } C_ A -> -. A = (/) ) )
52 51 con2d 
 |-  ( C e. _V -> ( A = (/) -> -. { C } C_ A ) )
53 52 pm4.71d 
 |-  ( C e. _V -> ( A = (/) <-> ( A = (/) /\ -. { C } C_ A ) ) )
54 eqimss2 
 |-  ( A = { C } -> { C } C_ A )
55 iman 
 |-  ( ( A = { C } -> { C } C_ A ) <-> -. ( A = { C } /\ -. { C } C_ A ) )
56 54 55 mpbi 
 |-  -. ( A = { C } /\ -. { C } C_ A )
57 56 biorfri 
 |-  ( ( A = (/) /\ -. { C } C_ A ) <-> ( ( A = (/) /\ -. { C } C_ A ) \/ ( A = { C } /\ -. { C } C_ A ) ) )
58 53 57 bitr2di 
 |-  ( C e. _V -> ( ( ( A = (/) /\ -. { C } C_ A ) \/ ( A = { C } /\ -. { C } C_ A ) ) <-> A = (/) ) )
59 49 58 bitrid 
 |-  ( C e. _V -> ( ( ( A = (/) \/ A = { C } ) /\ -. { C } C_ A ) <-> A = (/) ) )
60 48 59 bitrd 
 |-  ( C e. _V -> ( ( A C_ { C } /\ -. { C } C_ A ) <-> A = (/) ) )
61 20 bicomi 
 |-  ( ( B C_ { C } /\ { C } C_ B ) <-> B = { C } )
62 61 a1i 
 |-  ( C e. _V -> ( ( B C_ { C } /\ { C } C_ B ) <-> B = { C } ) )
63 60 62 anbi12d 
 |-  ( C e. _V -> ( ( ( A C_ { C } /\ -. { C } C_ A ) /\ ( B C_ { C } /\ { C } C_ B ) ) <-> ( A = (/) /\ B = { C } ) ) )
64 45 63 bitrid 
 |-  ( C e. _V -> ( ( ( A C_ { C } /\ B C_ { C } ) /\ ( -. { C } C_ A /\ { C } C_ B ) ) <-> ( A = (/) /\ B = { C } ) ) )
65 24 44 64 3orbi123d 
 |-  ( C e. _V -> ( ( ( ( A C_ { C } /\ B C_ { C } ) /\ ( { C } C_ A /\ { C } C_ B ) ) \/ ( ( A C_ { C } /\ B C_ { C } ) /\ ( { C } C_ A /\ -. { C } C_ B ) ) \/ ( ( A C_ { C } /\ B C_ { C } ) /\ ( -. { C } C_ A /\ { C } C_ B ) ) ) <-> ( ( A = { C } /\ B = { C } ) \/ ( A = { C } /\ B = (/) ) \/ ( A = (/) /\ B = { C } ) ) ) )
66 17 65 bitrid 
 |-  ( C e. _V -> ( ( ( A C_ { C } /\ B C_ { C } ) /\ ( { C } C_ A \/ { C } C_ B ) ) <-> ( ( A = { C } /\ B = { C } ) \/ ( A = { C } /\ B = (/) ) \/ ( A = (/) /\ B = { C } ) ) ) )
67 2 13 66 3bitrd 
 |-  ( C e. _V -> ( ( A u. B ) = { C } <-> ( ( A = { C } /\ B = { C } ) \/ ( A = { C } /\ B = (/) ) \/ ( A = (/) /\ B = { C } ) ) ) )
68 snprc 
 |-  ( -. C e. _V <-> { C } = (/) )
69 68 biimpi 
 |-  ( -. C e. _V -> { C } = (/) )
70 69 eqeq2d 
 |-  ( -. C e. _V -> ( ( A u. B ) = { C } <-> ( A u. 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 e. _V -> ( A = { C } <-> A = (/) ) )
75 69 eqeq2d 
 |-  ( -. C e. _V -> ( B = { C } <-> B = (/) ) )
76 74 75 anbi12d 
 |-  ( -. C e. _V -> ( ( A = { C } /\ B = { C } ) <-> ( A = (/) /\ B = (/) ) ) )
77 74 anbi1d 
 |-  ( -. C e. _V -> ( ( A = { C } /\ B = (/) ) <-> ( A = (/) /\ B = (/) ) ) )
78 76 77 orbi12d 
 |-  ( -. C e. _V -> ( ( ( A = { C } /\ B = { C } ) \/ ( A = { C } /\ B = (/) ) ) <-> ( ( A = (/) /\ B = (/) ) \/ ( A = (/) /\ B = (/) ) ) ) )
79 75 anbi2d 
 |-  ( -. C e. _V -> ( ( A = (/) /\ B = { C } ) <-> ( A = (/) /\ B = (/) ) ) )
80 78 79 orbi12d 
 |-  ( -. C e. _V -> ( ( ( ( A = { C } /\ B = { C } ) \/ ( A = { C } /\ B = (/) ) ) \/ ( A = (/) /\ B = { C } ) ) <-> ( ( ( A = (/) /\ B = (/) ) \/ ( A = (/) /\ B = (/) ) ) \/ ( A = (/) /\ B = (/) ) ) ) )
81 73 80 bitr4id 
 |-  ( -. C e. _V -> ( ( A = (/) /\ B = (/) ) <-> ( ( ( A = { C } /\ B = { C } ) \/ ( A = { C } /\ B = (/) ) ) \/ ( A = (/) /\ B = { C } ) ) ) )
82 un00 
 |-  ( ( A = (/) /\ B = (/) ) <-> ( A u. B ) = (/) )
83 82 bicomi 
 |-  ( ( A u. 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 e. _V -> ( ( A u. B ) = (/) <-> ( ( A = { C } /\ B = { C } ) \/ ( A = { C } /\ B = (/) ) \/ ( A = (/) /\ B = { C } ) ) ) )
86 70 85 bitrd 
 |-  ( -. C e. _V -> ( ( A u. B ) = { C } <-> ( ( A = { C } /\ B = { C } ) \/ ( A = { C } /\ B = (/) ) \/ ( A = (/) /\ B = { C } ) ) ) )
87 67 86 pm2.61i 
 |-  ( ( A u. B ) = { C } <-> ( ( A = { C } /\ B = { C } ) \/ ( A = { C } /\ B = (/) ) \/ ( A = (/) /\ B = { C } ) ) )