Metamath Proof Explorer

Theorem sstp

Description: The subsets of an unordered triple. (Contributed by Mario Carneiro, 2-Jul-2016)

Ref Expression
Assertion sstp 
|- ( A C_ { B , C , D } <-> ( ( ( A = (/) \/ A = { B } ) \/ ( A = { C } \/ A = { B , C } ) ) \/ ( ( A = { D } \/ A = { B , D } ) \/ ( A = { C , D } \/ A = { B , C , D } ) ) ) )

Proof

Step Hyp Ref Expression
1 df-tp 
 |-  { B , C , D } = ( { B , C } u. { D } )
2 1 sseq2i 
 |-  ( A C_ { B , C , D } <-> A C_ ( { B , C } u. { D } ) )
3 0ss 
 |-  (/) C_ A
4 3 biantrur 
 |-  ( A C_ ( { B , C } u. { D } ) <-> ( (/) C_ A /\ A C_ ( { B , C } u. { D } ) ) )
5 ssunsn2 
 |-  ( ( (/) C_ A /\ A C_ ( { B , C } u. { D } ) ) <-> ( ( (/) C_ A /\ A C_ { B , C } ) \/ ( ( (/) u. { D } ) C_ A /\ A C_ ( { B , C } u. { D } ) ) ) )
6 3 biantrur 
 |-  ( A C_ { B , C } <-> ( (/) C_ A /\ A C_ { B , C } ) )
7 sspr 
 |-  ( A C_ { B , C } <-> ( ( A = (/) \/ A = { B } ) \/ ( A = { C } \/ A = { B , C } ) ) )
8 6 7 bitr3i 
 |-  ( ( (/) C_ A /\ A C_ { B , C } ) <-> ( ( A = (/) \/ A = { B } ) \/ ( A = { C } \/ A = { B , C } ) ) )
9 uncom 
 |-  ( (/) u. { D } ) = ( { D } u. (/) )
10 un0 
 |-  ( { D } u. (/) ) = { D }
11 9 10 eqtri 
 |-  ( (/) u. { D } ) = { D }
12 11 sseq1i 
 |-  ( ( (/) u. { D } ) C_ A <-> { D } C_ A )
13 uncom 
 |-  ( { B , C } u. { D } ) = ( { D } u. { B , C } )
14 13 sseq2i 
 |-  ( A C_ ( { B , C } u. { D } ) <-> A C_ ( { D } u. { B , C } ) )
15 12 14 anbi12i 
 |-  ( ( ( (/) u. { D } ) C_ A /\ A C_ ( { B , C } u. { D } ) ) <-> ( { D } C_ A /\ A C_ ( { D } u. { B , C } ) ) )
16 ssunpr 
 |-  ( ( { D } C_ A /\ A C_ ( { D } u. { B , C } ) ) <-> ( ( A = { D } \/ A = ( { D } u. { B } ) ) \/ ( A = ( { D } u. { C } ) \/ A = ( { D } u. { B , C } ) ) ) )
17 uncom 
 |-  ( { D } u. { B } ) = ( { B } u. { D } )
18 df-pr 
 |-  { B , D } = ( { B } u. { D } )
19 17 18 eqtr4i 
 |-  ( { D } u. { B } ) = { B , D }
20 19 eqeq2i 
 |-  ( A = ( { D } u. { B } ) <-> A = { B , D } )
21 20 orbi2i 
 |-  ( ( A = { D } \/ A = ( { D } u. { B } ) ) <-> ( A = { D } \/ A = { B , D } ) )
22 uncom 
 |-  ( { D } u. { C } ) = ( { C } u. { D } )
23 df-pr 
 |-  { C , D } = ( { C } u. { D } )
24 22 23 eqtr4i 
 |-  ( { D } u. { C } ) = { C , D }
25 24 eqeq2i 
 |-  ( A = ( { D } u. { C } ) <-> A = { C , D } )
26 1 13 eqtr2i 
 |-  ( { D } u. { B , C } ) = { B , C , D }
27 26 eqeq2i 
 |-  ( A = ( { D } u. { B , C } ) <-> A = { B , C , D } )
28 25 27 orbi12i 
 |-  ( ( A = ( { D } u. { C } ) \/ A = ( { D } u. { B , C } ) ) <-> ( A = { C , D } \/ A = { B , C , D } ) )
29 21 28 orbi12i 
 |-  ( ( ( A = { D } \/ A = ( { D } u. { B } ) ) \/ ( A = ( { D } u. { C } ) \/ A = ( { D } u. { B , C } ) ) ) <-> ( ( A = { D } \/ A = { B , D } ) \/ ( A = { C , D } \/ A = { B , C , D } ) ) )
30 15 16 29 3bitri 
 |-  ( ( ( (/) u. { D } ) C_ A /\ A C_ ( { B , C } u. { D } ) ) <-> ( ( A = { D } \/ A = { B , D } ) \/ ( A = { C , D } \/ A = { B , C , D } ) ) )
31 8 30 orbi12i 
 |-  ( ( ( (/) C_ A /\ A C_ { B , C } ) \/ ( ( (/) u. { D } ) C_ A /\ A C_ ( { B , C } u. { D } ) ) ) <-> ( ( ( A = (/) \/ A = { B } ) \/ ( A = { C } \/ A = { B , C } ) ) \/ ( ( A = { D } \/ A = { B , D } ) \/ ( A = { C , D } \/ A = { B , C , D } ) ) ) )
32 5 31 bitri 
 |-  ( ( (/) C_ A /\ A C_ ( { B , C } u. { D } ) ) <-> ( ( ( A = (/) \/ A = { B } ) \/ ( A = { C } \/ A = { B , C } ) ) \/ ( ( A = { D } \/ A = { B , D } ) \/ ( A = { C , D } \/ A = { B , C , D } ) ) ) )
33 2 4 32 3bitri 
 |-  ( A C_ { B , C , D } <-> ( ( ( A = (/) \/ A = { B } ) \/ ( A = { C } \/ A = { B , C } ) ) \/ ( ( A = { D } \/ A = { B , D } ) \/ ( A = { C , D } \/ A = { B , C , D } ) ) ) )