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