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 disjsn ⊢ ( ( 𝐴 ∩ { 𝐷 } ) = ∅ ↔ ¬ 𝐷 ∈ 𝐴 )
17 disj3 ⊢ ( ( 𝐴 ∩ { 𝐷 } ) = ∅ ↔ 𝐴 = ( 𝐴 ∖ { 𝐷 } ) )
18 16 17 bitr3i ⊢ ( ¬ 𝐷 ∈ 𝐴 ↔ 𝐴 = ( 𝐴 ∖ { 𝐷 } ) )
19 sseq1 ⊢ ( 𝐴 = ( 𝐴 ∖ { 𝐷 } ) → ( 𝐴 ⊆ 𝐶 ↔ ( 𝐴 ∖ { 𝐷 } ) ⊆ 𝐶 ) )
20 18 19 sylbi ⊢ ( ¬ 𝐷 ∈ 𝐴 → ( 𝐴 ⊆ 𝐶 ↔ ( 𝐴 ∖ { 𝐷 } ) ⊆ 𝐶 ) )
21 uncom ⊢ ( { 𝐷 } ∪ 𝐶 ) = ( 𝐶 ∪ { 𝐷 } )
22 21 sseq2i ⊢ ( 𝐴 ⊆ ( { 𝐷 } ∪ 𝐶 ) ↔ 𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) )
23 ssundif ⊢ ( 𝐴 ⊆ ( { 𝐷 } ∪ 𝐶 ) ↔ ( 𝐴 ∖ { 𝐷 } ) ⊆ 𝐶 )
24 22 23 bitr3i ⊢ ( 𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ↔ ( 𝐴 ∖ { 𝐷 } ) ⊆ 𝐶 )
25 20 24 syl6rbbr ⊢ ( ¬ 𝐷 ∈ 𝐴 → ( 𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ↔ 𝐴 ⊆ 𝐶 ) )
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 syl6bb ⊢ ( ¬ 𝐷 ∈ 𝐴 → ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶 ) ↔ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶 ) ∨ ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ) ) )
35 26 34 bitrd ⊢ ( ¬ 𝐷 ∈ 𝐴 → ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ↔ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶 ) ∨ ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ) ) )
36 15 35 pm2.61i ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ↔ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐶 ) ∨ ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐶 ∪ { 𝐷 } ) ) ) )