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 0un ⊢ ( ∅ ∪ { 𝐵 , 𝐶 } ) = { 𝐵 , 𝐶 }
2 1 sseq2i ⊢ ( 𝐴 ⊆ ( ∅ ∪ { 𝐵 , 𝐶 } ) ↔ 𝐴 ⊆ { 𝐵 , 𝐶 } )
3 0ss ⊢ ∅ ⊆ 𝐴
4 3 biantrur ⊢ ( 𝐴 ⊆ ( ∅ ∪ { 𝐵 , 𝐶 } ) ↔ ( ∅ ⊆ 𝐴 ∧ 𝐴 ⊆ ( ∅ ∪ { 𝐵 , 𝐶 } ) ) )
5 2 4 bitr3i ⊢ ( 𝐴 ⊆ { 𝐵 , 𝐶 } ↔ ( ∅ ⊆ 𝐴 ∧ 𝐴 ⊆ ( ∅ ∪ { 𝐵 , 𝐶 } ) ) )
6 ssunpr ⊢ ( ( ∅ ⊆ 𝐴 ∧ 𝐴 ⊆ ( ∅ ∪ { 𝐵 , 𝐶 } ) ) ↔ ( ( 𝐴 = ∅ ∨ 𝐴 = ( ∅ ∪ { 𝐵 } ) ) ∨ ( 𝐴 = ( ∅ ∪ { 𝐶 } ) ∨ 𝐴 = ( ∅ ∪ { 𝐵 , 𝐶 } ) ) ) )
7 0un ⊢ ( ∅ ∪ { 𝐵 } ) = { 𝐵 }
8 7 eqeq2i ⊢ ( 𝐴 = ( ∅ ∪ { 𝐵 } ) ↔ 𝐴 = { 𝐵 } )
9 8 orbi2i ⊢ ( ( 𝐴 = ∅ ∨ 𝐴 = ( ∅ ∪ { 𝐵 } ) ) ↔ ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) )
10 0un ⊢ ( ∅ ∪ { 𝐶 } ) = { 𝐶 }
11 10 eqeq2i ⊢ ( 𝐴 = ( ∅ ∪ { 𝐶 } ) ↔ 𝐴 = { 𝐶 } )
12 1 eqeq2i ⊢ ( 𝐴 = ( ∅ ∪ { 𝐵 , 𝐶 } ) ↔ 𝐴 = { 𝐵 , 𝐶 } )
13 11 12 orbi12i ⊢ ( ( 𝐴 = ( ∅ ∪ { 𝐶 } ) ∨ 𝐴 = ( ∅ ∪ { 𝐵 , 𝐶 } ) ) ↔ ( 𝐴 = { 𝐶 } ∨ 𝐴 = { 𝐵 , 𝐶 } ) )
14 9 13 orbi12i ⊢ ( ( ( 𝐴 = ∅ ∨ 𝐴 = ( ∅ ∪ { 𝐵 } ) ) ∨ ( 𝐴 = ( ∅ ∪ { 𝐶 } ) ∨ 𝐴 = ( ∅ ∪ { 𝐵 , 𝐶 } ) ) ) ↔ ( ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) ∨ ( 𝐴 = { 𝐶 } ∨ 𝐴 = { 𝐵 , 𝐶 } ) ) )
15 5 6 14 3bitri ⊢ ( 𝐴 ⊆ { 𝐵 , 𝐶 } ↔ ( ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) ∨ ( 𝐴 = { 𝐶 } ∨ 𝐴 = { 𝐵 , 𝐶 } ) ) )