This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 } × { 2 , 7 } ) = ( { ⟨ 1 , 2 ⟩ , ⟨ 1 , 7 ⟩ } ∪ { ⟨ 5 , 2 ⟩ , ⟨ 5 , 7 ⟩ } )

Proof

Step Hyp Ref Expression
1 df-pr ⊢ { 1 , 5 } = ( { 1 } ∪ { 5 } )
2 df-pr ⊢ { 2 , 7 } = ( { 2 } ∪ { 7 } )
3 1 2 xpeq12i ⊢ ( { 1 , 5 } × { 2 , 7 } ) = ( ( { 1 } ∪ { 5 } ) × ( { 2 } ∪ { 7 } ) )
4 xpun ⊢ ( ( { 1 } ∪ { 5 } ) × ( { 2 } ∪ { 7 } ) ) = ( ( ( { 1 } × { 2 } ) ∪ ( { 1 } × { 7 } ) ) ∪ ( ( { 5 } × { 2 } ) ∪ ( { 5 } × { 7 } ) ) )
5 1ex ⊢ 1 ∈ V
6 2nn ⊢ 2 ∈ ℕ
7 6 elexi ⊢ 2 ∈ V
8 5 7 xpsn ⊢ ( { 1 } × { 2 } ) = { ⟨ 1 , 2 ⟩ }
9 7nn ⊢ 7 ∈ ℕ
10 9 elexi ⊢ 7 ∈ V
11 5 10 xpsn ⊢ ( { 1 } × { 7 } ) = { ⟨ 1 , 7 ⟩ }
12 8 11 uneq12i ⊢ ( ( { 1 } × { 2 } ) ∪ ( { 1 } × { 7 } ) ) = ( { ⟨ 1 , 2 ⟩ } ∪ { ⟨ 1 , 7 ⟩ } )
13 df-pr ⊢ { ⟨ 1 , 2 ⟩ , ⟨ 1 , 7 ⟩ } = ( { ⟨ 1 , 2 ⟩ } ∪ { ⟨ 1 , 7 ⟩ } )
14 12 13 eqtr4i ⊢ ( ( { 1 } × { 2 } ) ∪ ( { 1 } × { 7 } ) ) = { ⟨ 1 , 2 ⟩ , ⟨ 1 , 7 ⟩ }
15 5nn ⊢ 5 ∈ ℕ
16 15 elexi ⊢ 5 ∈ V
17 16 7 xpsn ⊢ ( { 5 } × { 2 } ) = { ⟨ 5 , 2 ⟩ }
18 16 10 xpsn ⊢ ( { 5 } × { 7 } ) = { ⟨ 5 , 7 ⟩ }
19 17 18 uneq12i ⊢ ( ( { 5 } × { 2 } ) ∪ ( { 5 } × { 7 } ) ) = ( { ⟨ 5 , 2 ⟩ } ∪ { ⟨ 5 , 7 ⟩ } )
20 df-pr ⊢ { ⟨ 5 , 2 ⟩ , ⟨ 5 , 7 ⟩ } = ( { ⟨ 5 , 2 ⟩ } ∪ { ⟨ 5 , 7 ⟩ } )
21 19 20 eqtr4i ⊢ ( ( { 5 } × { 2 } ) ∪ ( { 5 } × { 7 } ) ) = { ⟨ 5 , 2 ⟩ , ⟨ 5 , 7 ⟩ }
22 14 21 uneq12i ⊢ ( ( ( { 1 } × { 2 } ) ∪ ( { 1 } × { 7 } ) ) ∪ ( ( { 5 } × { 2 } ) ∪ ( { 5 } × { 7 } ) ) ) = ( { ⟨ 1 , 2 ⟩ , ⟨ 1 , 7 ⟩ } ∪ { ⟨ 5 , 2 ⟩ , ⟨ 5 , 7 ⟩ } )
23 3 4 22 3eqtri ⊢ ( { 1 , 5 } × { 2 , 7 } ) = ( { ⟨ 1 , 2 ⟩ , ⟨ 1 , 7 ⟩ } ∪ { ⟨ 5 , 2 ⟩ , ⟨ 5 , 7 ⟩ } )