Metamath Proof Explorer

Theorem ssunpr

Description: Possible values for a set sandwiched between another set and it plus a singleton. (Contributed by Mario Carneiro, 2-Jul-2016)

Ref Expression
Assertion ssunpr ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐵 ∪ { 𝐶 , 𝐷 } ) ) ↔ ( ( 𝐴 = 𝐵 ∨ 𝐴 = ( 𝐵 ∪ { 𝐶 } ) ) ∨ ( 𝐴 = ( 𝐵 ∪ { 𝐷 } ) ∨ 𝐴 = ( 𝐵 ∪ { 𝐶 , 𝐷 } ) ) ) )

Proof

Step Hyp Ref Expression
1 df-pr ⊢ { 𝐶 , 𝐷 } = ( { 𝐶 } ∪ { 𝐷 } )
2 1 uneq2i ⊢ ( 𝐵 ∪ { 𝐶 , 𝐷 } ) = ( 𝐵 ∪ ( { 𝐶 } ∪ { 𝐷 } ) )
3 unass ⊢ ( ( 𝐵 ∪ { 𝐶 } ) ∪ { 𝐷 } ) = ( 𝐵 ∪ ( { 𝐶 } ∪ { 𝐷 } ) )
4 2 3 eqtr4i ⊢ ( 𝐵 ∪ { 𝐶 , 𝐷 } ) = ( ( 𝐵 ∪ { 𝐶 } ) ∪ { 𝐷 } )
5 4 sseq2i ⊢ ( 𝐴 ⊆ ( 𝐵 ∪ { 𝐶 , 𝐷 } ) ↔ 𝐴 ⊆ ( ( 𝐵 ∪ { 𝐶 } ) ∪ { 𝐷 } ) )
6 5 anbi2i ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐵 ∪ { 𝐶 , 𝐷 } ) ) ↔ ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ ( ( 𝐵 ∪ { 𝐶 } ) ∪ { 𝐷 } ) ) )
7 ssunsn2 ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ ( ( 𝐵 ∪ { 𝐶 } ) ∪ { 𝐷 } ) ) ↔ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐵 ∪ { 𝐶 } ) ) ∨ ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ( 𝐵 ∪ { 𝐶 } ) ∪ { 𝐷 } ) ) ) )
8 ssunsn ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐵 ∪ { 𝐶 } ) ) ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = ( 𝐵 ∪ { 𝐶 } ) ) )
9 un23 ⊢ ( ( 𝐵 ∪ { 𝐶 } ) ∪ { 𝐷 } ) = ( ( 𝐵 ∪ { 𝐷 } ) ∪ { 𝐶 } )
10 9 sseq2i ⊢ ( 𝐴 ⊆ ( ( 𝐵 ∪ { 𝐶 } ) ∪ { 𝐷 } ) ↔ 𝐴 ⊆ ( ( 𝐵 ∪ { 𝐷 } ) ∪ { 𝐶 } ) )
11 10 anbi2i ⊢ ( ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ( 𝐵 ∪ { 𝐶 } ) ∪ { 𝐷 } ) ) ↔ ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ( 𝐵 ∪ { 𝐷 } ) ∪ { 𝐶 } ) ) )
12 ssunsn ⊢ ( ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ( 𝐵 ∪ { 𝐷 } ) ∪ { 𝐶 } ) ) ↔ ( 𝐴 = ( 𝐵 ∪ { 𝐷 } ) ∨ 𝐴 = ( ( 𝐵 ∪ { 𝐷 } ) ∪ { 𝐶 } ) ) )
13 4 9 eqtr2i ⊢ ( ( 𝐵 ∪ { 𝐷 } ) ∪ { 𝐶 } ) = ( 𝐵 ∪ { 𝐶 , 𝐷 } )
14 13 eqeq2i ⊢ ( 𝐴 = ( ( 𝐵 ∪ { 𝐷 } ) ∪ { 𝐶 } ) ↔ 𝐴 = ( 𝐵 ∪ { 𝐶 , 𝐷 } ) )
15 14 orbi2i ⊢ ( ( 𝐴 = ( 𝐵 ∪ { 𝐷 } ) ∨ 𝐴 = ( ( 𝐵 ∪ { 𝐷 } ) ∪ { 𝐶 } ) ) ↔ ( 𝐴 = ( 𝐵 ∪ { 𝐷 } ) ∨ 𝐴 = ( 𝐵 ∪ { 𝐶 , 𝐷 } ) ) )
16 11 12 15 3bitri ⊢ ( ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ( 𝐵 ∪ { 𝐶 } ) ∪ { 𝐷 } ) ) ↔ ( 𝐴 = ( 𝐵 ∪ { 𝐷 } ) ∨ 𝐴 = ( 𝐵 ∪ { 𝐶 , 𝐷 } ) ) )
17 8 16 orbi12i ⊢ ( ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐵 ∪ { 𝐶 } ) ) ∨ ( ( 𝐵 ∪ { 𝐷 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( ( 𝐵 ∪ { 𝐶 } ) ∪ { 𝐷 } ) ) ) ↔ ( ( 𝐴 = 𝐵 ∨ 𝐴 = ( 𝐵 ∪ { 𝐶 } ) ) ∨ ( 𝐴 = ( 𝐵 ∪ { 𝐷 } ) ∨ 𝐴 = ( 𝐵 ∪ { 𝐶 , 𝐷 } ) ) ) )
18 6 7 17 3bitri ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ ( 𝐵 ∪ { 𝐶 , 𝐷 } ) ) ↔ ( ( 𝐴 = 𝐵 ∨ 𝐴 = ( 𝐵 ∪ { 𝐶 } ) ) ∨ ( 𝐴 = ( 𝐵 ∪ { 𝐷 } ) ∨ 𝐴 = ( 𝐵 ∪ { 𝐶 , 𝐷 } ) ) ) )