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