Metamath Proof Explorer

Theorem orrabdioph

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

Ref Expression
Assertion 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 ) )

Proof

Step Hyp Ref Expression
1 unrab 
 |-  ( { t e. ( NN0 ^m ( 1 ... N ) ) | ph } u. { t e. ( NN0 ^m ( 1 ... N ) ) | ps } ) = { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph \/ ps ) }
2 diophun 
 |-  ( ( { 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 } u. { t e. ( NN0 ^m ( 1 ... N ) ) | ps } ) e. ( Dioph ` N ) )
3 1 2 eqeltrrid 
 |-  ( ( { 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 ) )