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 ⊢ F ∈ ⨉ x ∈ A B → F : A ⟶ ⋃ x ∈ A B

Proof

Step Hyp Ref Expression
1 elixp2 ⊢ F ∈ ⨉ x ∈ A B ↔ F ∈ V ∧ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B
2 ssiun2 ⊢ x ∈ A → B ⊆ ⋃ x ∈ A B
3 2 sseld ⊢ x ∈ A → F ⁡ x ∈ B → F ⁡ x ∈ ⋃ x ∈ A B
4 3 ralimia ⊢ ∀ x ∈ A F ⁡ x ∈ B → ∀ x ∈ A F ⁡ x ∈ ⋃ x ∈ A B
5 4 anim2i ⊢ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B → F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ ⋃ x ∈ A B
6 nfcv ⊢ Ⅎ _ x A
7 nfiu1 ⊢ Ⅎ _ x ⋃ x ∈ A B
8 nfcv ⊢ Ⅎ _ x F
9 6 7 8 ffnfvf ⊢ F : A ⟶ ⋃ x ∈ A B ↔ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ ⋃ x ∈ A B
10 5 9 sylibr ⊢ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B → F : A ⟶ ⋃ x ∈ A B
11 10 3adant1 ⊢ F ∈ V ∧ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B → F : A ⟶ ⋃ x ∈ A B
12 1 11 sylbi ⊢ F ∈ ⨉ x ∈ A B → F : A ⟶ ⋃ x ∈ A B