dprdw

Description: The property of being a finitely supported function in the family S . (Contributed by Mario Carneiro, 25-Apr-2016) (Revised by AV, 11-Jul-2019)

	Ref	Expression
Hypotheses	dprdff.w	$⊢ W = \{h \in \underset{i \in I}{⨉} S (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
	dprdff.1	$⊢ φ \to G dom DProd S$
	dprdff.2	$⊢ φ \to dom S = I$
Assertion	dprdw	$⊢ φ \to (F \in W \leftrightarrow (F Fn I \land \forall x \in I F (x) \in S (x) \land {finSupp}_{\underset{˙}{0}} (F)))$

Proof

Step	Hyp	Ref	Expression
1		dprdff.w	$⊢ W = \{h \in \underset{i \in I}{⨉} S (i) \| {finSupp}_{\underset{˙}{0}} (h)\}$
2		dprdff.1	$⊢ φ \to G dom DProd S$
3		dprdff.2	$⊢ φ \to dom S = I$
4		elex	$⊢ F \in \underset{i \in I}{⨉} S (i) \to F \in V$
5	4	a1i	$⊢ φ \to (F \in \underset{i \in I}{⨉} S (i) \to F \in V)$
6	2 3	dprddomcld	$⊢ φ \to I \in V$
7		fnex	$⊢ (F Fn I \land I \in V) \to F \in V$
8	7	expcom	$⊢ I \in V \to (F Fn I \to F \in V)$
9	6 8	syl	$⊢ φ \to (F Fn I \to F \in V)$
10	9	adantrd	$⊢ φ \to ((F Fn I \land \forall x \in I F (x) \in S (x)) \to F \in V)$
11		fveq2	$⊢ i = x \to S (i) = S (x)$
12	11	cbvixpv	$⊢ \underset{i \in I}{⨉} S (i) = \underset{x \in I}{⨉} S (x)$
13	12	eleq2i	$⊢ F \in \underset{i \in I}{⨉} S (i) \leftrightarrow F \in \underset{x \in I}{⨉} S (x)$
14		elixp2	$⊢ F \in \underset{x \in I}{⨉} S (x) \leftrightarrow (F \in V \land F Fn I \land \forall x \in I F (x) \in S (x))$
15		3anass	$⊢ (F \in V \land F Fn I \land \forall x \in I F (x) \in S (x)) \leftrightarrow (F \in V \land (F Fn I \land \forall x \in I F (x) \in S (x)))$
16	13 14 15	3bitri	$⊢ F \in \underset{i \in I}{⨉} S (i) \leftrightarrow (F \in V \land (F Fn I \land \forall x \in I F (x) \in S (x)))$
17	16	baib	$⊢ F \in V \to (F \in \underset{i \in I}{⨉} S (i) \leftrightarrow (F Fn I \land \forall x \in I F (x) \in S (x)))$
18	17	a1i	$⊢ φ \to (F \in V \to (F \in \underset{i \in I}{⨉} S (i) \leftrightarrow (F Fn I \land \forall x \in I F (x) \in S (x))))$
19	5 10 18	pm5.21ndd	$⊢ φ \to (F \in \underset{i \in I}{⨉} S (i) \leftrightarrow (F Fn I \land \forall x \in I F (x) \in S (x)))$
20	19	anbi1d	$⊢ φ \to ((F \in \underset{i \in I}{⨉} S (i) \land {finSupp}_{\underset{˙}{0}} (F)) \leftrightarrow ((F Fn I \land \forall x \in I F (x) \in S (x)) \land {finSupp}_{\underset{˙}{0}} (F)))$
21		breq1	$⊢ h = F \to ({finSupp}_{\underset{˙}{0}} (h) \leftrightarrow {finSupp}_{\underset{˙}{0}} (F))$
22	21 1	elrab2	$⊢ F \in W \leftrightarrow (F \in \underset{i \in I}{⨉} S (i) \land {finSupp}_{\underset{˙}{0}} (F))$
23		df-3an	$⊢ (F Fn I \land \forall x \in I F (x) \in S (x) \land {finSupp}_{\underset{˙}{0}} (F)) \leftrightarrow ((F Fn I \land \forall x \in I F (x) \in S (x)) \land {finSupp}_{\underset{˙}{0}} (F))$
24	20 22 23	3bitr4g	$⊢ φ \to (F \in W \leftrightarrow (F Fn I \land \forall x \in I F (x) \in S (x) \land {finSupp}_{\underset{˙}{0}} (F)))$

Metamath Proof Explorer

Theorem dprdw

Proof