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 uncom
 |-  ( { D } u. C ) = ( C u. { D } )
17 16 sseq2i
 |-  ( A C_ ( { D } u. C ) <-> A C_ ( C u. { D } ) )
18 ssundif
 |-  ( A C_ ( { D } u. C ) <-> ( A \ { D } ) C_ C )
19 17 18 bitr3i
 |-  ( A C_ ( C u. { D } ) <-> ( A \ { D } ) C_ C )
20 disjsn
 |-  ( ( A i^i { D } ) = (/) <-> -. D e. A )
21 disj3
 |-  ( ( A i^i { D } ) = (/) <-> A = ( A \ { D } ) )
22 20 21 bitr3i
 |-  ( -. D e. A <-> A = ( A \ { D } ) )
23 sseq1
 |-  ( A = ( A \ { D } ) -> ( A C_ C <-> ( A \ { D } ) C_ C ) )
24 22 23 sylbi
 |-  ( -. D e. A -> ( A C_ C <-> ( A \ { D } ) C_ C ) )
25 19 24 bitr4id
 |-  ( -. 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 bitrdi
 |-  ( -. 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 } ) ) ) )