# 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}\in {V}\to \left({F}\in \underset{{x}\in {A}}{⨉}{B}↔{F}:{A}⟶{B}\right)$

### Proof

Step Hyp Ref Expression
1 ixpfn ${⊢}{F}\in \underset{{x}\in {A}}{⨉}{B}\to {F}Fn{A}$
2 elixp2 ${⊢}{F}\in \underset{{x}\in {A}}{⨉}{B}↔\left({F}\in \mathrm{V}\wedge {F}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\right)$
3 2 simp3bi ${⊢}{F}\in \underset{{x}\in {A}}{⨉}{B}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}$
4 ffnfv ${⊢}{F}:{A}⟶{B}↔\left({F}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}\right)$
5 1 3 4 sylanbrc ${⊢}{F}\in \underset{{x}\in {A}}{⨉}{B}\to {F}:{A}⟶{B}$
6 elex ${⊢}{F}\in {V}\to {F}\in \mathrm{V}$
7 6 adantr ${⊢}\left({F}\in {V}\wedge {F}:{A}⟶{B}\right)\to {F}\in \mathrm{V}$
8 ffn ${⊢}{F}:{A}⟶{B}\to {F}Fn{A}$
9 8 adantl ${⊢}\left({F}\in {V}\wedge {F}:{A}⟶{B}\right)\to {F}Fn{A}$
10 4 simprbi ${⊢}{F}:{A}⟶{B}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}$
11 10 adantl ${⊢}\left({F}\in {V}\wedge {F}:{A}⟶{B}\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {B}$
12 7 9 11 2 syl3anbrc ${⊢}\left({F}\in {V}\wedge {F}:{A}⟶{B}\right)\to {F}\in \underset{{x}\in {A}}{⨉}{B}$
13 12 ex ${⊢}{F}\in {V}\to \left({F}:{A}⟶{B}\to {F}\in \underset{{x}\in {A}}{⨉}{B}\right)$
14 5 13 impbid2 ${⊢}{F}\in {V}\to \left({F}\in \underset{{x}\in {A}}{⨉}{B}↔{F}:{A}⟶{B}\right)$