mptelixpg

Description: Condition for an explicit member of an indexed product. (Contributed by Stefan O'Rear, 4-Jan-2015)

		Ref	Expression
	Assertion	mptelixpg	$⊢ I \in V \to ((x \in I ⟼ J) \in \underset{x \in I}{⨉} K \leftrightarrow \forall x \in I J \in K)$

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ I \in V \to I \in V$
2		nfcv	$⊢ \underline{Ⅎ} y K$
3		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ K$
4		csbeq1a	$⊢ x = y \to K = ⦋ y / x ⦌ K$
5	2 3 4	cbvixp	$⊢ \underset{x \in I}{⨉} K = \underset{y \in I}{⨉} ⦋ y / x ⦌ K$
6	5	eleq2i	$⊢ (x \in I ⟼ J) \in \underset{x \in I}{⨉} K \leftrightarrow (x \in I ⟼ J) \in \underset{y \in I}{⨉} ⦋ y / x ⦌ K$
7		elixp2	$⊢ (x \in I ⟼ J) \in \underset{y \in I}{⨉} ⦋ y / x ⦌ K \leftrightarrow ((x \in I ⟼ J) \in V \land (x \in I ⟼ J) Fn I \land \forall y \in I (x \in I ⟼ J) (y) \in ⦋ y / x ⦌ K)$
8		3anass	$⊢ ((x \in I ⟼ J) \in V \land (x \in I ⟼ J) Fn I \land \forall y \in I (x \in I ⟼ J) (y) \in ⦋ y / x ⦌ K) \leftrightarrow ((x \in I ⟼ J) \in V \land ((x \in I ⟼ J) Fn I \land \forall y \in I (x \in I ⟼ J) (y) \in ⦋ y / x ⦌ K))$
9	6 7 8	3bitri	$⊢ (x \in I ⟼ J) \in \underset{x \in I}{⨉} K \leftrightarrow ((x \in I ⟼ J) \in V \land ((x \in I ⟼ J) Fn I \land \forall y \in I (x \in I ⟼ J) (y) \in ⦋ y / x ⦌ K))$
10		eqid	$⊢ (x \in I ⟼ J) = (x \in I ⟼ J)$
11	10	fnmpt	$⊢ \forall x \in I J \in K \to (x \in I ⟼ J) Fn I$
12	10	fvmpt2	$⊢ (x \in I \land J \in K) \to (x \in I ⟼ J) (x) = J$
13		simpr	$⊢ (x \in I \land J \in K) \to J \in K$
14	12 13	eqeltrd	$⊢ (x \in I \land J \in K) \to (x \in I ⟼ J) (x) \in K$
15	14	ralimiaa	$⊢ \forall x \in I J \in K \to \forall x \in I (x \in I ⟼ J) (x) \in K$
16	11 15	jca	$⊢ \forall x \in I J \in K \to ((x \in I ⟼ J) Fn I \land \forall x \in I (x \in I ⟼ J) (x) \in K)$
17		dffn2	$⊢ (x \in I ⟼ J) Fn I \leftrightarrow (x \in I ⟼ J) : I ⟶ V$
18	10	fmpt	$⊢ \forall x \in I J \in V \leftrightarrow (x \in I ⟼ J) : I ⟶ V$
19	10	fvmpt2	$⊢ (x \in I \land J \in V) \to (x \in I ⟼ J) (x) = J$
20	19	eleq1d	$⊢ (x \in I \land J \in V) \to ((x \in I ⟼ J) (x) \in K \leftrightarrow J \in K)$
21	20	biimpd	$⊢ (x \in I \land J \in V) \to ((x \in I ⟼ J) (x) \in K \to J \in K)$
22	21	ralimiaa	$⊢ \forall x \in I J \in V \to \forall x \in I ((x \in I ⟼ J) (x) \in K \to J \in K)$
23		ralim	$⊢ \forall x \in I ((x \in I ⟼ J) (x) \in K \to J \in K) \to (\forall x \in I (x \in I ⟼ J) (x) \in K \to \forall x \in I J \in K)$
24	22 23	syl	$⊢ \forall x \in I J \in V \to (\forall x \in I (x \in I ⟼ J) (x) \in K \to \forall x \in I J \in K)$
25	18 24	sylbir	$⊢ (x \in I ⟼ J) : I ⟶ V \to (\forall x \in I (x \in I ⟼ J) (x) \in K \to \forall x \in I J \in K)$
26	17 25	sylbi	$⊢ (x \in I ⟼ J) Fn I \to (\forall x \in I (x \in I ⟼ J) (x) \in K \to \forall x \in I J \in K)$
27	26	imp	$⊢ ((x \in I ⟼ J) Fn I \land \forall x \in I (x \in I ⟼ J) (x) \in K) \to \forall x \in I J \in K$
28	16 27	impbii	$⊢ \forall x \in I J \in K \leftrightarrow ((x \in I ⟼ J) Fn I \land \forall x \in I (x \in I ⟼ J) (x) \in K)$
29		nfv	$⊢ Ⅎ y (x \in I ⟼ J) (x) \in K$
30		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in I ⟼ J) (y)$
31	30 3	nfel	$⊢ Ⅎ x (x \in I ⟼ J) (y) \in ⦋ y / x ⦌ K$
32		fveq2	$⊢ x = y \to (x \in I ⟼ J) (x) = (x \in I ⟼ J) (y)$
33	32 4	eleq12d	$⊢ x = y \to ((x \in I ⟼ J) (x) \in K \leftrightarrow (x \in I ⟼ J) (y) \in ⦋ y / x ⦌ K)$
34	29 31 33	cbvralw	$⊢ \forall x \in I (x \in I ⟼ J) (x) \in K \leftrightarrow \forall y \in I (x \in I ⟼ J) (y) \in ⦋ y / x ⦌ K$
35	34	anbi2i	$⊢ ((x \in I ⟼ J) Fn I \land \forall x \in I (x \in I ⟼ J) (x) \in K) \leftrightarrow ((x \in I ⟼ J) Fn I \land \forall y \in I (x \in I ⟼ J) (y) \in ⦋ y / x ⦌ K)$
36	28 35	bitri	$⊢ \forall x \in I J \in K \leftrightarrow ((x \in I ⟼ J) Fn I \land \forall y \in I (x \in I ⟼ J) (y) \in ⦋ y / x ⦌ K)$
37		mptexg	$⊢ I \in V \to (x \in I ⟼ J) \in V$
38	37	biantrurd	$⊢ I \in V \to (((x \in I ⟼ J) Fn I \land \forall y \in I (x \in I ⟼ J) (y) \in ⦋ y / x ⦌ K) \leftrightarrow ((x \in I ⟼ J) \in V \land ((x \in I ⟼ J) Fn I \land \forall y \in I (x \in I ⟼ J) (y) \in ⦋ y / x ⦌ K)))$
39	36 38	bitr2id	$⊢ I \in V \to (((x \in I ⟼ J) \in V \land ((x \in I ⟼ J) Fn I \land \forall y \in I (x \in I ⟼ J) (y) \in ⦋ y / x ⦌ K)) \leftrightarrow \forall x \in I J \in K)$
40	9 39	syl5bb	$⊢ I \in V \to ((x \in I ⟼ J) \in \underset{x \in I}{⨉} K \leftrightarrow \forall x \in I J \in K)$
41	1 40	syl	$⊢ I \in V \to ((x \in I ⟼ J) \in \underset{x \in I}{⨉} K \leftrightarrow \forall x \in I J \in K)$

Metamath Proof Explorer

Theorem mptelixpg

Proof