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

Metamath Proof Explorer

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 𝑥 ∈ 𝐴 𝐵 → 𝐹 : 𝐴 ⟶ ∪ 𝑥 ∈ 𝐴 𝐵 )