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 (F \in \underset{x \in A}{⨉} B \leftrightarrow F : A ⟶ B)$

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 \leftrightarrow (F \in V \land F Fn A \land \forall x \in A F (x) \in B)$
3	2	simp3bi	$⊢ F \in \underset{x \in A}{⨉} B \to \forall x \in A F (x) \in B$
4		ffnfv	$⊢ F : A ⟶ B \leftrightarrow (F Fn A \land \forall x \in A F (x) \in B)$
5	1 3 4	sylanbrc	$⊢ F \in \underset{x \in A}{⨉} B \to F : A ⟶ B$
6		elex	$⊢ F \in V \to F \in V$
7	6	adantr	$⊢ (F \in V \land F : A ⟶ B) \to F \in V$
8		ffn	$⊢ F : A ⟶ B \to F Fn A$
9	8	adantl	$⊢ (F \in V \land F : A ⟶ B) \to F Fn A$
10	4	simprbi	$⊢ F : A ⟶ B \to \forall x \in A F (x) \in B$
11	10	adantl	$⊢ (F \in V \land F : A ⟶ B) \to \forall x \in A F (x) \in B$
12	7 9 11 2	syl3anbrc	$⊢ (F \in V \land F : A ⟶ B) \to F \in \underset{x \in A}{⨉} B$
13	12	ex	$⊢ F \in V \to (F : A ⟶ B \to F \in \underset{x \in A}{⨉} B)$
14	5 13	impbid2	$⊢ F \in V \to (F \in \underset{x \in A}{⨉} B \leftrightarrow F : A ⟶ B)$

Metamath Proof Explorer