Metamath Proof Explorer

Theorem sstp

Description: The subsets of an unordered triple. (Contributed by Mario Carneiro, 2-Jul-2016)

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

Proof

Step Hyp Ref Expression
1 df-tp ⊢ { 𝐵 , 𝐶 , 𝐷 } = ( { 𝐵 , 𝐶 } ∪ { 𝐷 } )
2 1 sseq2i ⊢ ( 𝐴 ⊆ { 𝐵 , 𝐶 , 𝐷 } ↔ 𝐴 ⊆ ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) )
3 0ss ⊢ ∅ ⊆ 𝐴
4 3 biantrur ⊢ ( 𝐴 ⊆ ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) ↔ ( ∅ ⊆ 𝐴 ∧ 𝐴 ⊆ ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) )
5 ssunsn2 ⊢ ( ( ∅ ⊆ 𝐴 ∧ 𝐴 ⊆ ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) ↔ ( ( ∅ ⊆ 𝐴 ∧ 𝐴 ⊆ { 𝐵 , 𝐶 } ) ∨ ( ( ∅ ∪ { 𝐷 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) ) )
6 3 biantrur ⊢ ( 𝐴 ⊆ { 𝐵 , 𝐶 } ↔ ( ∅ ⊆ 𝐴 ∧ 𝐴 ⊆ { 𝐵 , 𝐶 } ) )
7 sspr ⊢ ( 𝐴 ⊆ { 𝐵 , 𝐶 } ↔ ( ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) ∨ ( 𝐴 = { 𝐶 } ∨ 𝐴 = { 𝐵 , 𝐶 } ) ) )
8 6 7 bitr3i ⊢ ( ( ∅ ⊆ 𝐴 ∧ 𝐴 ⊆ { 𝐵 , 𝐶 } ) ↔ ( ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) ∨ ( 𝐴 = { 𝐶 } ∨ 𝐴 = { 𝐵 , 𝐶 } ) ) )
9 0un ⊢ ( ∅ ∪ { 𝐷 } ) = { 𝐷 }
10 9 sseq1i ⊢ ( ( ∅ ∪ { 𝐷 } ) ⊆ 𝐴 ↔ { 𝐷 } ⊆ 𝐴 )
11 uncom ⊢ ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) = ( { 𝐷 } ∪ { 𝐵 , 𝐶 } )
12 11 sseq2i ⊢ ( 𝐴 ⊆ ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) ↔ 𝐴 ⊆ ( { 𝐷 } ∪ { 𝐵 , 𝐶 } ) )
13 10 12 anbi12i ⊢ ( ( ( ∅ ∪ { 𝐷 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) ↔ ( { 𝐷 } ⊆ 𝐴 ∧ 𝐴 ⊆ ( { 𝐷 } ∪ { 𝐵 , 𝐶 } ) ) )
14 ssunpr ⊢ ( ( { 𝐷 } ⊆ 𝐴 ∧ 𝐴 ⊆ ( { 𝐷 } ∪ { 𝐵 , 𝐶 } ) ) ↔ ( ( 𝐴 = { 𝐷 } ∨ 𝐴 = ( { 𝐷 } ∪ { 𝐵 } ) ) ∨ ( 𝐴 = ( { 𝐷 } ∪ { 𝐶 } ) ∨ 𝐴 = ( { 𝐷 } ∪ { 𝐵 , 𝐶 } ) ) ) )
15 uncom ⊢ ( { 𝐷 } ∪ { 𝐵 } ) = ( { 𝐵 } ∪ { 𝐷 } )
16 df-pr ⊢ { 𝐵 , 𝐷 } = ( { 𝐵 } ∪ { 𝐷 } )
17 15 16 eqtr4i ⊢ ( { 𝐷 } ∪ { 𝐵 } ) = { 𝐵 , 𝐷 }
18 17 eqeq2i ⊢ ( 𝐴 = ( { 𝐷 } ∪ { 𝐵 } ) ↔ 𝐴 = { 𝐵 , 𝐷 } )
19 18 orbi2i ⊢ ( ( 𝐴 = { 𝐷 } ∨ 𝐴 = ( { 𝐷 } ∪ { 𝐵 } ) ) ↔ ( 𝐴 = { 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐷 } ) )
20 uncom ⊢ ( { 𝐷 } ∪ { 𝐶 } ) = ( { 𝐶 } ∪ { 𝐷 } )
21 df-pr ⊢ { 𝐶 , 𝐷 } = ( { 𝐶 } ∪ { 𝐷 } )
22 20 21 eqtr4i ⊢ ( { 𝐷 } ∪ { 𝐶 } ) = { 𝐶 , 𝐷 }
23 22 eqeq2i ⊢ ( 𝐴 = ( { 𝐷 } ∪ { 𝐶 } ) ↔ 𝐴 = { 𝐶 , 𝐷 } )
24 1 11 eqtr2i ⊢ ( { 𝐷 } ∪ { 𝐵 , 𝐶 } ) = { 𝐵 , 𝐶 , 𝐷 }
25 24 eqeq2i ⊢ ( 𝐴 = ( { 𝐷 } ∪ { 𝐵 , 𝐶 } ) ↔ 𝐴 = { 𝐵 , 𝐶 , 𝐷 } )
26 23 25 orbi12i ⊢ ( ( 𝐴 = ( { 𝐷 } ∪ { 𝐶 } ) ∨ 𝐴 = ( { 𝐷 } ∪ { 𝐵 , 𝐶 } ) ) ↔ ( 𝐴 = { 𝐶 , 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐶 , 𝐷 } ) )
27 19 26 orbi12i ⊢ ( ( ( 𝐴 = { 𝐷 } ∨ 𝐴 = ( { 𝐷 } ∪ { 𝐵 } ) ) ∨ ( 𝐴 = ( { 𝐷 } ∪ { 𝐶 } ) ∨ 𝐴 = ( { 𝐷 } ∪ { 𝐵 , 𝐶 } ) ) ) ↔ ( ( 𝐴 = { 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐷 } ) ∨ ( 𝐴 = { 𝐶 , 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐶 , 𝐷 } ) ) )
28 13 14 27 3bitri ⊢ ( ( ( ∅ ∪ { 𝐷 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) ↔ ( ( 𝐴 = { 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐷 } ) ∨ ( 𝐴 = { 𝐶 , 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐶 , 𝐷 } ) ) )
29 8 28 orbi12i ⊢ ( ( ( ∅ ⊆ 𝐴 ∧ 𝐴 ⊆ { 𝐵 , 𝐶 } ) ∨ ( ( ∅ ∪ { 𝐷 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) ) ↔ ( ( ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) ∨ ( 𝐴 = { 𝐶 } ∨ 𝐴 = { 𝐵 , 𝐶 } ) ) ∨ ( ( 𝐴 = { 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐷 } ) ∨ ( 𝐴 = { 𝐶 , 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐶 , 𝐷 } ) ) ) )
30 5 29 bitri ⊢ ( ( ∅ ⊆ 𝐴 ∧ 𝐴 ⊆ ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) ↔ ( ( ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) ∨ ( 𝐴 = { 𝐶 } ∨ 𝐴 = { 𝐵 , 𝐶 } ) ) ∨ ( ( 𝐴 = { 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐷 } ) ∨ ( 𝐴 = { 𝐶 , 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐶 , 𝐷 } ) ) ) )
31 2 4 30 3bitri ⊢ ( 𝐴 ⊆ { 𝐵 , 𝐶 , 𝐷 } ↔ ( ( ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) ∨ ( 𝐴 = { 𝐶 } ∨ 𝐴 = { 𝐵 , 𝐶 } ) ) ∨ ( ( 𝐴 = { 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐷 } ) ∨ ( 𝐴 = { 𝐶 , 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐶 , 𝐷 } ) ) ) )