Metamath Proof Explorer

Theorem ssunsn2

Description: The property of being sandwiched between two sets naturally splits under union with a singleton. This is the induction hypothesis for the determination of large powersets such as pwtp . (Contributed by Mario Carneiro, 2-Jul-2016)

Ref Expression
Assertion ssunsn2 
|- ( ( B C_ A /\ A C_ ( C u. { D } ) ) <-> ( ( B C_ A /\ A C_ C ) \/ ( ( B u. { D } ) C_ A /\ A C_ ( C u. { D } ) ) ) )

Proof

Step Hyp Ref Expression
1 snssi 
 |-  ( D e. A -> { D } C_ A )
2 unss 
 |-  ( ( B C_ A /\ { D } C_ A ) <-> ( B u. { D } ) C_ A )
3 2 bicomi 
 |-  ( ( B u. { D } ) C_ A <-> ( B C_ A /\ { D } C_ A ) )
4 3 rbaibr 
 |-  ( { D } C_ A -> ( B C_ A <-> ( B u. { D } ) C_ A ) )
5 1 4 syl 
 |-  ( D e. A -> ( B C_ A <-> ( B u. { D } ) C_ A ) )
6 5 anbi1d 
 |-  ( D e. A -> ( ( B C_ A /\ A C_ ( C u. { D } ) ) <-> ( ( B u. { D } ) C_ A /\ A C_ ( C u. { D } ) ) ) )
7 2 biimpi 
 |-  ( ( B C_ A /\ { D } C_ A ) -> ( B u. { D } ) C_ A )
8 7 expcom 
 |-  ( { D } C_ A -> ( B C_ A -> ( B u. { D } ) C_ A ) )
9 1 8 syl 
 |-  ( D e. A -> ( B C_ A -> ( B u. { D } ) C_ A ) )
10 ssun3 
 |-  ( A C_ C -> A C_ ( C u. { D } ) )
11 10 a1i 
 |-  ( D e. A -> ( A C_ C -> A C_ ( C u. { D } ) ) )
12 9 11 anim12d 
 |-  ( D e. A -> ( ( B C_ A /\ A C_ C ) -> ( ( B u. { D } ) C_ A /\ A C_ ( C u. { D } ) ) ) )
13 pm4.72 
 |-  ( ( ( B C_ A /\ A C_ C ) -> ( ( B u. { D } ) C_ A /\ A C_ ( C u. { D } ) ) ) <-> ( ( ( B u. { D } ) C_ A /\ A C_ ( C u. { D } ) ) <-> ( ( B C_ A /\ A C_ C ) \/ ( ( B u. { D } ) C_ A /\ A C_ ( C u. { D } ) ) ) ) )
14 12 13 sylib 
 |-  ( D e. A -> ( ( ( B u. { D } ) C_ A /\ A C_ ( C u. { D } ) ) <-> ( ( B C_ A /\ A C_ C ) \/ ( ( B u. { D } ) C_ A /\ A C_ ( C u. { D } ) ) ) ) )
15 6 14 bitrd 
 |-  ( D e. A -> ( ( B C_ A /\ A C_ ( C u. { D } ) ) <-> ( ( B C_ A /\ A C_ C ) \/ ( ( B u. { D } ) C_ A /\ A C_ ( C u. { D } ) ) ) ) )
16 disjsn 
 |-  ( ( A i^i { D } ) = (/) <-> -. D e. A )
17 disj3 
 |-  ( ( A i^i { D } ) = (/) <-> A = ( A \ { D } ) )
18 16 17 bitr3i 
 |-  ( -. D e. A <-> A = ( A \ { D } ) )
19 sseq1 
 |-  ( A = ( A \ { D } ) -> ( A C_ C <-> ( A \ { D } ) C_ C ) )
20 18 19 sylbi 
 |-  ( -. D e. A -> ( A C_ C <-> ( A \ { D } ) C_ C ) )
21 uncom 
 |-  ( { D } u. C ) = ( C u. { D } )
22 21 sseq2i 
 |-  ( A C_ ( { D } u. C ) <-> A C_ ( C u. { D } ) )
23 ssundif 
 |-  ( A C_ ( { D } u. C ) <-> ( A \ { D } ) C_ C )
24 22 23 bitr3i 
 |-  ( A C_ ( C u. { D } ) <-> ( A \ { D } ) C_ C )
25 20 24 syl6rbbr 
 |-  ( -. D e. A -> ( A C_ ( C u. { D } ) <-> A C_ C ) )
26 25 anbi2d 
 |-  ( -. D e. A -> ( ( B C_ A /\ A C_ ( C u. { D } ) ) <-> ( B C_ A /\ A C_ C ) ) )
27 3 simplbi 
 |-  ( ( B u. { D } ) C_ A -> B C_ A )
28 27 a1i 
 |-  ( -. D e. A -> ( ( B u. { D } ) C_ A -> B C_ A ) )
29 25 biimpd 
 |-  ( -. D e. A -> ( A C_ ( C u. { D } ) -> A C_ C ) )
30 28 29 anim12d 
 |-  ( -. D e. A -> ( ( ( B u. { D } ) C_ A /\ A C_ ( C u. { D } ) ) -> ( B C_ A /\ A C_ C ) ) )
31 pm4.72 
 |-  ( ( ( ( B u. { D } ) C_ A /\ A C_ ( C u. { D } ) ) -> ( B C_ A /\ A C_ C ) ) <-> ( ( B C_ A /\ A C_ C ) <-> ( ( ( B u. { D } ) C_ A /\ A C_ ( C u. { D } ) ) \/ ( B C_ A /\ A C_ C ) ) ) )
32 30 31 sylib 
 |-  ( -. D e. A -> ( ( B C_ A /\ A C_ C ) <-> ( ( ( B u. { D } ) C_ A /\ A C_ ( C u. { D } ) ) \/ ( B C_ A /\ A C_ C ) ) ) )
33 orcom 
 |-  ( ( ( ( B u. { D } ) C_ A /\ A C_ ( C u. { D } ) ) \/ ( B C_ A /\ A C_ C ) ) <-> ( ( B C_ A /\ A C_ C ) \/ ( ( B u. { D } ) C_ A /\ A C_ ( C u. { D } ) ) ) )
34 32 33 syl6bb 
 |-  ( -. D e. A -> ( ( B C_ A /\ A C_ C ) <-> ( ( B C_ A /\ A C_ C ) \/ ( ( B u. { D } ) C_ A /\ A C_ ( C u. { D } ) ) ) ) )
35 26 34 bitrd 
 |-  ( -. D e. A -> ( ( B C_ A /\ A C_ ( C u. { D } ) ) <-> ( ( B C_ A /\ A C_ C ) \/ ( ( B u. { D } ) C_ A /\ A C_ ( C u. { D } ) ) ) ) )
36 15 35 pm2.61i 
 |-  ( ( B C_ A /\ A C_ ( C u. { D } ) ) <-> ( ( B C_ A /\ A C_ C ) \/ ( ( B u. { D } ) C_ A /\ A C_ ( C u. { D } ) ) ) )