Metamath Proof Explorer

Theorem 3orrabdioph

Description: Diophantine set builder for ternary disjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014)

Ref Expression
Assertion 3orrabdioph 
|- ( ( { t e. ( NN0 ^m ( 1 ... N ) ) | ph } e. ( Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ps } e. ( Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ch } e. ( Dioph ` N ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph \/ ps \/ ch ) } e. ( Dioph ` N ) )

Proof

Step Hyp Ref Expression
1 df-3or 
 |-  ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )
2 1 rabbii 
 |-  { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph \/ ps \/ ch ) } = { t e. ( NN0 ^m ( 1 ... N ) ) | ( ( ph \/ ps ) \/ ch ) }
3 orrabdioph 
 |-  ( ( { t e. ( NN0 ^m ( 1 ... N ) ) | ph } e. ( Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ps } e. ( Dioph ` N ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph \/ ps ) } e. ( Dioph ` N ) )
4 orrabdioph 
 |-  ( ( { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph \/ ps ) } e. ( Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ch } e. ( Dioph ` N ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( ( ph \/ ps ) \/ ch ) } e. ( Dioph ` N ) )
5 3 4 sylan 
 |-  ( ( ( { t e. ( NN0 ^m ( 1 ... N ) ) | ph } e. ( Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ps } e. ( Dioph ` N ) ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ch } e. ( Dioph ` N ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( ( ph \/ ps ) \/ ch ) } e. ( Dioph ` N ) )
6 2 5 eqeltrid 
 |-  ( ( ( { t e. ( NN0 ^m ( 1 ... N ) ) | ph } e. ( Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ps } e. ( Dioph ` N ) ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ch } e. ( Dioph ` N ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph \/ ps \/ ch ) } e. ( Dioph ` N ) )
7 6 3impa 
 |-  ( ( { t e. ( NN0 ^m ( 1 ... N ) ) | ph } e. ( Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ps } e. ( Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ch } e. ( Dioph ` N ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph \/ ps \/ ch ) } e. ( Dioph ` N ) )