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 ⟩ } )