Metamath Proof Explorer

Theorem elixpconstg

Description: Membership in an infinite Cartesian product of a constant B . (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Assertion elixpconstg ⊢ F ∈ V → F ∈ ⨉ x ∈ A B ↔ F : A ⟶ B

Proof

Step Hyp Ref Expression
1 ixpfn ⊢ F ∈ ⨉ x ∈ A B → F Fn A
2 elixp2 ⊢ F ∈ ⨉ x ∈ A B ↔ F ∈ V ∧ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B
3 2 simp3bi ⊢ F ∈ ⨉ x ∈ A B → ∀ x ∈ A F ⁡ x ∈ B
4 ffnfv ⊢ F : A ⟶ B ↔ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B
5 1 3 4 sylanbrc ⊢ F ∈ ⨉ x ∈ A B → F : A ⟶ B
6 elex ⊢ F ∈ V → F ∈ V
7 6 adantr ⊢ F ∈ V ∧ F : A ⟶ B → F ∈ V
8 ffn ⊢ F : A ⟶ B → F Fn A
9 8 adantl ⊢ F ∈ V ∧ F : A ⟶ B → F Fn A
10 4 simprbi ⊢ F : A ⟶ B → ∀ x ∈ A F ⁡ x ∈ B
11 10 adantl ⊢ F ∈ V ∧ F : A ⟶ B → ∀ x ∈ A F ⁡ x ∈ B
12 7 9 11 2 syl3anbrc ⊢ F ∈ V ∧ F : A ⟶ B → F ∈ ⨉ x ∈ A B
13 12 ex ⊢ F ∈ V → F : A ⟶ B → F ∈ ⨉ x ∈ A B
14 5 13 impbid2 ⊢ F ∈ V → F ∈ ⨉ x ∈ A B ↔ F : A ⟶ B