Theorem ixpf

Description: A member of an infinite Cartesian product maps to the indexed union of the product argument. Remark in Enderton p. 54. (Contributed by NM, 28-Sep-2006)

	Ref	Expression
Assertion	ixpf	⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐵 → 𝐹 : 𝐴 ⟶ ∪ 𝑥 ∈ 𝐴 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		elixp2	⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) )
2		ssiun2	⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
3	2	sseld	⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 → ( 𝐹 ‘ 𝑥 ) ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
4	3	ralimia	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
5	4	anim2i	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
6		nfcv	⊢ Ⅎ 𝑥 𝐴
7		nfiu1	⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 𝐵
8		nfcv	⊢ Ⅎ 𝑥 𝐹
9	6 7 8	ffnfvf	⊢ ( 𝐹 : 𝐴 ⟶ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
10	5 9	sylibr	⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → 𝐹 : 𝐴 ⟶ ∪ 𝑥 ∈ 𝐴 𝐵 )
11	10	3adant1	⊢ ( ( 𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 ) → 𝐹 : 𝐴 ⟶ ∪ 𝑥 ∈ 𝐴 𝐵 )
12	1 11	sylbi	⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐴 𝐵 → 𝐹 : 𝐴 ⟶ ∪ 𝑥 ∈ 𝐴 𝐵 )