df-ixp

Description: Definition of infinite Cartesian product of Enderton p. 54. Enderton uses a bold "X" with x e. A written underneath or as a subscript, as does Stoll p. 47. Some books use a capital pi, but we will reserve that notation for products of numbers. Usually B represents a class expression containing x free and thus can be thought of as B ( x ) . Normally, x is not free in A , although this is not a requirement of the definition. (Contributed by NM, 28-Sep-2006)

		Ref	Expression
	Assertion	df-ixp	⊢ X 𝑥 ∈ 𝐴 𝐵 = { 𝑓 ∣ ( 𝑓 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		cA	⊢ 𝐴
2		cB	⊢ 𝐵
3	0 1 2	cixp	⊢ X 𝑥 ∈ 𝐴 𝐵
4		vf	⊢ 𝑓
5	4	cv	⊢ 𝑓
6	0	cv	⊢ 𝑥
7	6 1	wcel	⊢ 𝑥 ∈ 𝐴
8	7 0	cab	⊢ { 𝑥 ∣ 𝑥 ∈ 𝐴 }
9	5 8	wfn	⊢ 𝑓 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 }
10	6 5	cfv	⊢ ( 𝑓 ‘ 𝑥 )
11	10 2	wcel	⊢ ( 𝑓 ‘ 𝑥 ) ∈ 𝐵
12	11 0 1	wral	⊢ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵
13	9 12	wa	⊢ ( 𝑓 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 )
14	13 4	cab	⊢ { 𝑓 ∣ ( 𝑓 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) }
15	3 14	wceq	⊢ X 𝑥 ∈ 𝐴 𝐵 = { 𝑓 ∣ ( 𝑓 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) }

Metamath Proof Explorer

Definition df-ixp

Detailed syntax breakdown