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 ( ( 𝐵𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ↔ ( ( 𝐵𝐴𝐴𝐶 ) ∨ ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ) )

Proof

Step Hyp Ref Expression
1 snssi ( 𝐷𝐴 → { 𝐷 } ⊆ 𝐴 )
2 unss ( ( 𝐵𝐴 ∧ { 𝐷 } ⊆ 𝐴 ) ↔ ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴 )
3 2 bicomi ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴 ↔ ( 𝐵𝐴 ∧ { 𝐷 } ⊆ 𝐴 ) )
4 3 rbaibr ( { 𝐷 } ⊆ 𝐴 → ( 𝐵𝐴 ↔ ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴 ) )
5 1 4 syl ( 𝐷𝐴 → ( 𝐵𝐴 ↔ ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴 ) )
6 5 anbi1d ( 𝐷𝐴 → ( ( 𝐵𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ↔ ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ) )
7 2 biimpi ( ( 𝐵𝐴 ∧ { 𝐷 } ⊆ 𝐴 ) → ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴 )
8 7 expcom ( { 𝐷 } ⊆ 𝐴 → ( 𝐵𝐴 → ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴 ) )
9 1 8 syl ( 𝐷𝐴 → ( 𝐵𝐴 → ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴 ) )
10 ssun3 ( 𝐴𝐶𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) )
11 10 a1i ( 𝐷𝐴 → ( 𝐴𝐶𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) )
12 9 11 anim12d ( 𝐷𝐴 → ( ( 𝐵𝐴𝐴𝐶 ) → ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ) )
13 pm4.72 ( ( ( 𝐵𝐴𝐴𝐶 ) → ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ) ↔ ( ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ↔ ( ( 𝐵𝐴𝐴𝐶 ) ∨ ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ) ) )
14 12 13 sylib ( 𝐷𝐴 → ( ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ↔ ( ( 𝐵𝐴𝐴𝐶 ) ∨ ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ) ) )
15 6 14 bitrd ( 𝐷𝐴 → ( ( 𝐵𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ↔ ( ( 𝐵𝐴𝐴𝐶 ) ∨ ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ) ) )
16 uncom ( { 𝐷 } ∪ 𝐶 ) = ( 𝐶 ∪ { 𝐷 } )
17 16 sseq2i ( 𝐴 ⊆ ( { 𝐷 } ∪ 𝐶 ) ↔ 𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) )
18 ssundif ( 𝐴 ⊆ ( { 𝐷 } ∪ 𝐶 ) ↔ ( 𝐴 ∖ { 𝐷 } ) ⊆ 𝐶 )
19 17 18 bitr3i ( 𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ↔ ( 𝐴 ∖ { 𝐷 } ) ⊆ 𝐶 )
20 disjsn ( ( 𝐴 ∩ { 𝐷 } ) = ∅ ↔ ¬ 𝐷𝐴 )
21 disj3 ( ( 𝐴 ∩ { 𝐷 } ) = ∅ ↔ 𝐴 = ( 𝐴 ∖ { 𝐷 } ) )
22 20 21 bitr3i ( ¬ 𝐷𝐴𝐴 = ( 𝐴 ∖ { 𝐷 } ) )
23 sseq1 ( 𝐴 = ( 𝐴 ∖ { 𝐷 } ) → ( 𝐴𝐶 ↔ ( 𝐴 ∖ { 𝐷 } ) ⊆ 𝐶 ) )
24 22 23 sylbi ( ¬ 𝐷𝐴 → ( 𝐴𝐶 ↔ ( 𝐴 ∖ { 𝐷 } ) ⊆ 𝐶 ) )
25 19 24 bitr4id ( ¬ 𝐷𝐴 → ( 𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ↔ 𝐴𝐶 ) )
26 25 anbi2d ( ¬ 𝐷𝐴 → ( ( 𝐵𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ↔ ( 𝐵𝐴𝐴𝐶 ) ) )
27 3 simplbi ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴𝐵𝐴 )
28 27 a1i ( ¬ 𝐷𝐴 → ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴𝐵𝐴 ) )
29 25 biimpd ( ¬ 𝐷𝐴 → ( 𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) → 𝐴𝐶 ) )
30 28 29 anim12d ( ¬ 𝐷𝐴 → ( ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) → ( 𝐵𝐴𝐴𝐶 ) ) )
31 pm4.72 ( ( ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) → ( 𝐵𝐴𝐴𝐶 ) ) ↔ ( ( 𝐵𝐴𝐴𝐶 ) ↔ ( ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ∨ ( 𝐵𝐴𝐴𝐶 ) ) ) )
32 30 31 sylib ( ¬ 𝐷𝐴 → ( ( 𝐵𝐴𝐴𝐶 ) ↔ ( ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ∨ ( 𝐵𝐴𝐴𝐶 ) ) ) )
33 orcom ( ( ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ∨ ( 𝐵𝐴𝐴𝐶 ) ) ↔ ( ( 𝐵𝐴𝐴𝐶 ) ∨ ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ) )
34 32 33 bitrdi ( ¬ 𝐷𝐴 → ( ( 𝐵𝐴𝐴𝐶 ) ↔ ( ( 𝐵𝐴𝐴𝐶 ) ∨ ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ) ) )
35 26 34 bitrd ( ¬ 𝐷𝐴 → ( ( 𝐵𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ↔ ( ( 𝐵𝐴𝐴𝐶 ) ∨ ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ) ) )
36 15 35 pm2.61i ( ( 𝐵𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ↔ ( ( 𝐵𝐴𝐴𝐶 ) ∨ ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ) )