elixp2

Description: Membership in an infinite Cartesian product. See df-ixp for discussion of the notation. (Contributed by NM, 28-Sep-2006)

		Ref	Expression
	Assertion	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)$

Step	Hyp	Ref	Expression
1		fneq1	$⊢ f = F \to (f Fn A \leftrightarrow F Fn A)$
2		fveq1	$⊢ f = F \to f (x) = F (x)$
3	2	eleq1d	$⊢ f = F \to (f (x) \in B \leftrightarrow F (x) \in B)$
4	3	ralbidv	$⊢ f = F \to (\forall x \in A f (x) \in B \leftrightarrow \forall x \in A F (x) \in B)$
5	1 4	anbi12d	$⊢ f = F \to ((f Fn A \land \forall x \in A f (x) \in B) \leftrightarrow (F Fn A \land \forall x \in A F (x) \in B))$
6		dfixp	$⊢ \underset{x \in A}{⨉} B = \{f \| (f Fn A \land \forall x \in A f (x) \in B)\}$
7	5 6	elab2g	$⊢ F \in V \to (F \in \underset{x \in A}{⨉} B \leftrightarrow (F Fn A \land \forall x \in A F (x) \in B))$
8	7	pm5.32i	$⊢ (F \in V \land F \in \underset{x \in A}{⨉} B) \leftrightarrow (F \in V \land (F Fn A \land \forall x \in A F (x) \in B))$
9		elex	$⊢ F \in \underset{x \in A}{⨉} B \to F \in V$
10	9	pm4.71ri	$⊢ F \in \underset{x \in A}{⨉} B \leftrightarrow (F \in V \land F \in \underset{x \in A}{⨉} B)$
11		3anass	$⊢ (F \in V \land F Fn A \land \forall x \in A F (x) \in B) \leftrightarrow (F \in V \land (F Fn A \land \forall x \in A F (x) \in B))$
12	8 10 11	3bitr4i	$⊢ F \in \underset{x \in A}{⨉} B \leftrightarrow (F \in V \land F Fn A \land \forall x \in A F (x) \in B)$

Metamath Proof Explorer