Metamath Proof Explorer

Theorem ex-xp

Description: Example for df-xp . Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Assertion ex-xp 
|- ( { 1 , 5 } X. { 2 , 7 } ) = ( { <. 1 , 2 >. , <. 1 , 7 >. } u. { <. 5 , 2 >. , <. 5 , 7 >. } )

Proof

Step Hyp Ref Expression
1 df-pr 
 |-  { 1 , 5 } = ( { 1 } u. { 5 } )
2 df-pr 
 |-  { 2 , 7 } = ( { 2 } u. { 7 } )
3 1 2 xpeq12i 
 |-  ( { 1 , 5 } X. { 2 , 7 } ) = ( ( { 1 } u. { 5 } ) X. ( { 2 } u. { 7 } ) )
4 xpun 
 |-  ( ( { 1 } u. { 5 } ) X. ( { 2 } u. { 7 } ) ) = ( ( ( { 1 } X. { 2 } ) u. ( { 1 } X. { 7 } ) ) u. ( ( { 5 } X. { 2 } ) u. ( { 5 } X. { 7 } ) ) )
5 1ex 
 |-  1 e. _V
6 2nn 
 |-  2 e. NN
7 6 elexi 
 |-  2 e. _V
8 5 7 xpsn 
 |-  ( { 1 } X. { 2 } ) = { <. 1 , 2 >. }
9 7nn 
 |-  7 e. NN
10 9 elexi 
 |-  7 e. _V
11 5 10 xpsn 
 |-  ( { 1 } X. { 7 } ) = { <. 1 , 7 >. }
12 8 11 uneq12i 
 |-  ( ( { 1 } X. { 2 } ) u. ( { 1 } X. { 7 } ) ) = ( { <. 1 , 2 >. } u. { <. 1 , 7 >. } )
13 df-pr 
 |-  { <. 1 , 2 >. , <. 1 , 7 >. } = ( { <. 1 , 2 >. } u. { <. 1 , 7 >. } )
14 12 13 eqtr4i 
 |-  ( ( { 1 } X. { 2 } ) u. ( { 1 } X. { 7 } ) ) = { <. 1 , 2 >. , <. 1 , 7 >. }
15 5nn 
 |-  5 e. NN
16 15 elexi 
 |-  5 e. _V
17 16 7 xpsn 
 |-  ( { 5 } X. { 2 } ) = { <. 5 , 2 >. }
18 16 10 xpsn 
 |-  ( { 5 } X. { 7 } ) = { <. 5 , 7 >. }
19 17 18 uneq12i 
 |-  ( ( { 5 } X. { 2 } ) u. ( { 5 } X. { 7 } ) ) = ( { <. 5 , 2 >. } u. { <. 5 , 7 >. } )
20 df-pr 
 |-  { <. 5 , 2 >. , <. 5 , 7 >. } = ( { <. 5 , 2 >. } u. { <. 5 , 7 >. } )
21 19 20 eqtr4i 
 |-  ( ( { 5 } X. { 2 } ) u. ( { 5 } X. { 7 } ) ) = { <. 5 , 2 >. , <. 5 , 7 >. }
22 14 21 uneq12i 
 |-  ( ( ( { 1 } X. { 2 } ) u. ( { 1 } X. { 7 } ) ) u. ( ( { 5 } X. { 2 } ) u. ( { 5 } X. { 7 } ) ) ) = ( { <. 1 , 2 >. , <. 1 , 7 >. } u. { <. 5 , 2 >. , <. 5 , 7 >. } )
23 3 4 22 3eqtri 
 |-  ( { 1 , 5 } X. { 2 , 7 } ) = ( { <. 1 , 2 >. , <. 1 , 7 >. } u. { <. 5 , 2 >. , <. 5 , 7 >. } )