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 uncom ⊢ ( ∅ ∪ { 𝐷 } ) = ( { 𝐷 } ∪ ∅ )
10 un0 ⊢ ( { 𝐷 } ∪ ∅ ) = { 𝐷 }
11 9 10 eqtri ⊢ ( ∅ ∪ { 𝐷 } ) = { 𝐷 }
12 11 sseq1i ⊢ ( ( ∅ ∪ { 𝐷 } ) ⊆ 𝐴 ↔ { 𝐷 } ⊆ 𝐴 )
13 uncom ⊢ ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) = ( { 𝐷 } ∪ { 𝐵 , 𝐶 } )
14 13 sseq2i ⊢ ( 𝐴 ⊆ ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) ↔ 𝐴 ⊆ ( { 𝐷 } ∪ { 𝐵 , 𝐶 } ) )
15 12 14 anbi12i ⊢ ( ( ( ∅ ∪ { 𝐷 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) ↔ ( { 𝐷 } ⊆ 𝐴 ∧ 𝐴 ⊆ ( { 𝐷 } ∪ { 𝐵 , 𝐶 } ) ) )
16 ssunpr ⊢ ( ( { 𝐷 } ⊆ 𝐴 ∧ 𝐴 ⊆ ( { 𝐷 } ∪ { 𝐵 , 𝐶 } ) ) ↔ ( ( 𝐴 = { 𝐷 } ∨ 𝐴 = ( { 𝐷 } ∪ { 𝐵 } ) ) ∨ ( 𝐴 = ( { 𝐷 } ∪ { 𝐶 } ) ∨ 𝐴 = ( { 𝐷 } ∪ { 𝐵 , 𝐶 } ) ) ) )
17 uncom ⊢ ( { 𝐷 } ∪ { 𝐵 } ) = ( { 𝐵 } ∪ { 𝐷 } )
18 df-pr ⊢ { 𝐵 , 𝐷 } = ( { 𝐵 } ∪ { 𝐷 } )
19 17 18 eqtr4i ⊢ ( { 𝐷 } ∪ { 𝐵 } ) = { 𝐵 , 𝐷 }
20 19 eqeq2i ⊢ ( 𝐴 = ( { 𝐷 } ∪ { 𝐵 } ) ↔ 𝐴 = { 𝐵 , 𝐷 } )
21 20 orbi2i ⊢ ( ( 𝐴 = { 𝐷 } ∨ 𝐴 = ( { 𝐷 } ∪ { 𝐵 } ) ) ↔ ( 𝐴 = { 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐷 } ) )
22 uncom ⊢ ( { 𝐷 } ∪ { 𝐶 } ) = ( { 𝐶 } ∪ { 𝐷 } )
23 df-pr ⊢ { 𝐶 , 𝐷 } = ( { 𝐶 } ∪ { 𝐷 } )
24 22 23 eqtr4i ⊢ ( { 𝐷 } ∪ { 𝐶 } ) = { 𝐶 , 𝐷 }
25 24 eqeq2i ⊢ ( 𝐴 = ( { 𝐷 } ∪ { 𝐶 } ) ↔ 𝐴 = { 𝐶 , 𝐷 } )
26 1 13 eqtr2i ⊢ ( { 𝐷 } ∪ { 𝐵 , 𝐶 } ) = { 𝐵 , 𝐶 , 𝐷 }
27 26 eqeq2i ⊢ ( 𝐴 = ( { 𝐷 } ∪ { 𝐵 , 𝐶 } ) ↔ 𝐴 = { 𝐵 , 𝐶 , 𝐷 } )
28 25 27 orbi12i ⊢ ( ( 𝐴 = ( { 𝐷 } ∪ { 𝐶 } ) ∨ 𝐴 = ( { 𝐷 } ∪ { 𝐵 , 𝐶 } ) ) ↔ ( 𝐴 = { 𝐶 , 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐶 , 𝐷 } ) )
29 21 28 orbi12i ⊢ ( ( ( 𝐴 = { 𝐷 } ∨ 𝐴 = ( { 𝐷 } ∪ { 𝐵 } ) ) ∨ ( 𝐴 = ( { 𝐷 } ∪ { 𝐶 } ) ∨ 𝐴 = ( { 𝐷 } ∪ { 𝐵 , 𝐶 } ) ) ) ↔ ( ( 𝐴 = { 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐷 } ) ∨ ( 𝐴 = { 𝐶 , 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐶 , 𝐷 } ) ) )
30 15 16 29 3bitri ⊢ ( ( ( ∅ ∪ { 𝐷 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) ↔ ( ( 𝐴 = { 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐷 } ) ∨ ( 𝐴 = { 𝐶 , 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐶 , 𝐷 } ) ) )
31 8 30 orbi12i ⊢ ( ( ( ∅ ⊆ 𝐴 ∧ 𝐴 ⊆ { 𝐵 , 𝐶 } ) ∨ ( ( ∅ ∪ { 𝐷 } ) ⊆ 𝐴 ∧ 𝐴 ⊆ ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) ) ↔ ( ( ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) ∨ ( 𝐴 = { 𝐶 } ∨ 𝐴 = { 𝐵 , 𝐶 } ) ) ∨ ( ( 𝐴 = { 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐷 } ) ∨ ( 𝐴 = { 𝐶 , 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐶 , 𝐷 } ) ) ) )
32 5 31 bitri ⊢ ( ( ∅ ⊆ 𝐴 ∧ 𝐴 ⊆ ( { 𝐵 , 𝐶 } ∪ { 𝐷 } ) ) ↔ ( ( ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) ∨ ( 𝐴 = { 𝐶 } ∨ 𝐴 = { 𝐵 , 𝐶 } ) ) ∨ ( ( 𝐴 = { 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐷 } ) ∨ ( 𝐴 = { 𝐶 , 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐶 , 𝐷 } ) ) ) )
33 2 4 32 3bitri ⊢ ( 𝐴 ⊆ { 𝐵 , 𝐶 , 𝐷 } ↔ ( ( ( 𝐴 = ∅ ∨ 𝐴 = { 𝐵 } ) ∨ ( 𝐴 = { 𝐶 } ∨ 𝐴 = { 𝐵 , 𝐶 } ) ) ∨ ( ( 𝐴 = { 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐷 } ) ∨ ( 𝐴 = { 𝐶 , 𝐷 } ∨ 𝐴 = { 𝐵 , 𝐶 , 𝐷 } ) ) ) )