This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sspr

Description: The subsets of a pair. (Contributed by NM, 16-Mar-2006) (Proof shortened by Mario Carneiro, 2-Jul-2016)

Ref Expression
Assertion sspr ( 𝐴 ⊆ { 𝐵 , 𝐶 } ↔ ( ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) ∨ ( 𝐴 = { 𝐶 } ∨ 𝐴 = { 𝐵 , 𝐶 } ) ) )

Proof

Step Hyp Ref Expression
1 uncom ⊢ ( ∅ ∪ { 𝐵 , 𝐶 } ) = ( { 𝐵 , 𝐶 } ∪ ∅ )
2 un0 ⊢ ( { 𝐵 , 𝐶 } ∪ ∅ ) = { 𝐵 , 𝐶 }
3 1 2 eqtri ⊢ ( ∅ ∪ { 𝐵 , 𝐶 } ) = { 𝐵 , 𝐶 }
4 3 sseq2i ⊢ ( 𝐴 ⊆ ( ∅ ∪ { 𝐵 , 𝐶 } ) ↔ 𝐴 ⊆ { 𝐵 , 𝐶 } )
5 0ss ⊢ ∅ ⊆ 𝐴
6 5 biantrur ⊢ ( 𝐴 ⊆ ( ∅ ∪ { 𝐵 , 𝐶 } ) ↔ ( ∅ ⊆ 𝐴 ∧ 𝐴 ⊆ ( ∅ ∪ { 𝐵 , 𝐶 } ) ) )
7 4 6 bitr3i ⊢ ( 𝐴 ⊆ { 𝐵 , 𝐶 } ↔ ( ∅ ⊆ 𝐴 ∧ 𝐴 ⊆ ( ∅ ∪ { 𝐵 , 𝐶 } ) ) )
8 ssunpr ⊢ ( ( ∅ ⊆ 𝐴 ∧ 𝐴 ⊆ ( ∅ ∪ { 𝐵 , 𝐶 } ) ) ↔ ( ( 𝐴 = ∅ ∨ 𝐴 = ( ∅ ∪ { 𝐵 } ) ) ∨ ( 𝐴 = ( ∅ ∪ { 𝐶 } ) ∨ 𝐴 = ( ∅ ∪ { 𝐵 , 𝐶 } ) ) ) )
9 uncom ⊢ ( ∅ ∪ { 𝐵 } ) = ( { 𝐵 } ∪ ∅ )
10 un0 ⊢ ( { 𝐵 } ∪ ∅ ) = { 𝐵 }
11 9 10 eqtri ⊢ ( ∅ ∪ { 𝐵 } ) = { 𝐵 }
12 11 eqeq2i ⊢ ( 𝐴 = ( ∅ ∪ { 𝐵 } ) ↔ 𝐴 = { 𝐵 } )
13 12 orbi2i ⊢ ( ( 𝐴 = ∅ ∨ 𝐴 = ( ∅ ∪ { 𝐵 } ) ) ↔ ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) )
14 uncom ⊢ ( ∅ ∪ { 𝐶 } ) = ( { 𝐶 } ∪ ∅ )
15 un0 ⊢ ( { 𝐶 } ∪ ∅ ) = { 𝐶 }
16 14 15 eqtri ⊢ ( ∅ ∪ { 𝐶 } ) = { 𝐶 }
17 16 eqeq2i ⊢ ( 𝐴 = ( ∅ ∪ { 𝐶 } ) ↔ 𝐴 = { 𝐶 } )
18 3 eqeq2i ⊢ ( 𝐴 = ( ∅ ∪ { 𝐵 , 𝐶 } ) ↔ 𝐴 = { 𝐵 , 𝐶 } )
19 17 18 orbi12i ⊢ ( ( 𝐴 = ( ∅ ∪ { 𝐶 } ) ∨ 𝐴 = ( ∅ ∪ { 𝐵 , 𝐶 } ) ) ↔ ( 𝐴 = { 𝐶 } ∨ 𝐴 = { 𝐵 , 𝐶 } ) )
20 13 19 orbi12i ⊢ ( ( ( 𝐴 = ∅ ∨ 𝐴 = ( ∅ ∪ { 𝐵 } ) ) ∨ ( 𝐴 = ( ∅ ∪ { 𝐶 } ) ∨ 𝐴 = ( ∅ ∪ { 𝐵 , 𝐶 } ) ) ) ↔ ( ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) ∨ ( 𝐴 = { 𝐶 } ∨ 𝐴 = { 𝐵 , 𝐶 } ) ) )
21 7 8 20 3bitri ⊢ ( 𝐴 ⊆ { 𝐵 , 𝐶 } ↔ ( ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) ∨ ( 𝐴 = { 𝐶 } ∨ 𝐴 = { 𝐵 , 𝐶 } ) ) )