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 e. V -> ( F e. X_ x e. A B <-> F : A --> B ) )

Proof

Step Hyp Ref Expression
1 ixpfn 
 |-  ( F e. X_ x e. A B -> F Fn A )
2 elixp2 
 |-  ( F e. X_ x e. A B <-> ( F e. _V /\ F Fn A /\ A. x e. A ( F ` x ) e. B ) )
3 2 simp3bi 
 |-  ( F e. X_ x e. A B -> A. x e. A ( F ` x ) e. B )
4 ffnfv 
 |-  ( F : A --> B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )
5 1 3 4 sylanbrc 
 |-  ( F e. X_ x e. A B -> F : A --> B )
6 elex 
 |-  ( F e. V -> F e. _V )
7 6 adantr 
 |-  ( ( F e. V /\ F : A --> B ) -> F e. _V )
8 ffn 
 |-  ( F : A --> B -> F Fn A )
9 8 adantl 
 |-  ( ( F e. V /\ F : A --> B ) -> F Fn A )
10 4 simprbi 
 |-  ( F : A --> B -> A. x e. A ( F ` x ) e. B )
11 10 adantl 
 |-  ( ( F e. V /\ F : A --> B ) -> A. x e. A ( F ` x ) e. B )
12 7 9 11 2 syl3anbrc 
 |-  ( ( F e. V /\ F : A --> B ) -> F e. X_ x e. A B )
13 12 ex 
 |-  ( F e. V -> ( F : A --> B -> F e. X_ x e. A B ) )
14 5 13 impbid2 
 |-  ( F e. V -> ( F e. X_ x e. A B <-> F : A --> B ) )