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	⊢ ( 𝐴 ⊆ { 𝐵 , 𝐶 } ↔ ( ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) ∨ ( 𝐴 = { 𝐶 } ∨ 𝐴 = { 𝐵 , 𝐶 } ) ) )