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	⊢ 𝑊 = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 }
	dprdff.1	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
	dprdff.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
Assertion	dprdw	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑊 ↔ ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ∧ 𝐹 finSupp 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dprdff.w	⊢ 𝑊 = { ℎ ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∣ ℎ finSupp 0 }
2		dprdff.1	⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
3		dprdff.2	⊢ ( 𝜑 → dom 𝑆 = 𝐼 )
4		elex	⊢ ( 𝐹 ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) → 𝐹 ∈ V )
5	4	a1i	⊢ ( 𝜑 → ( 𝐹 ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) → 𝐹 ∈ V ) )
6	2 3	dprddomcld	⊢ ( 𝜑 → 𝐼 ∈ V )
7		fnex	⊢ ( ( 𝐹 Fn 𝐼 ∧ 𝐼 ∈ V ) → 𝐹 ∈ V )
8	7	expcom	⊢ ( 𝐼 ∈ V → ( 𝐹 Fn 𝐼 → 𝐹 ∈ V ) )
9	6 8	syl	⊢ ( 𝜑 → ( 𝐹 Fn 𝐼 → 𝐹 ∈ V ) )
10	9	adantrd	⊢ ( 𝜑 → ( ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ) → 𝐹 ∈ V ) )
11		fveq2	⊢ ( 𝑖 = 𝑥 → ( 𝑆 ‘ 𝑖 ) = ( 𝑆 ‘ 𝑥 ) )
12	11	cbvixpv	⊢ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) = X 𝑥 ∈ 𝐼 ( 𝑆 ‘ 𝑥 )
13	12	eleq2i	⊢ ( 𝐹 ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ↔ 𝐹 ∈ X 𝑥 ∈ 𝐼 ( 𝑆 ‘ 𝑥 ) )
14		elixp2	⊢ ( 𝐹 ∈ X 𝑥 ∈ 𝐼 ( 𝑆 ‘ 𝑥 ) ↔ ( 𝐹 ∈ V ∧ 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ) )
15		3anass	⊢ ( ( 𝐹 ∈ V ∧ 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ) ↔ ( 𝐹 ∈ V ∧ ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ) ) )
16	13 14 15	3bitri	⊢ ( 𝐹 ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ↔ ( 𝐹 ∈ V ∧ ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ) ) )
17	16	baib	⊢ ( 𝐹 ∈ V → ( 𝐹 ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ↔ ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ) ) )
18	17	a1i	⊢ ( 𝜑 → ( 𝐹 ∈ V → ( 𝐹 ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ↔ ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ) ) ) )
19	5 10 18	pm5.21ndd	⊢ ( 𝜑 → ( 𝐹 ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ↔ ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ) ) )
20	19	anbi1d	⊢ ( 𝜑 → ( ( 𝐹 ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∧ 𝐹 finSupp 0 ) ↔ ( ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ) ∧ 𝐹 finSupp 0 ) ) )
21		breq1	⊢ ( ℎ = 𝐹 → ( ℎ finSupp 0 ↔ 𝐹 finSupp 0 ) )
22	21 1	elrab2	⊢ ( 𝐹 ∈ 𝑊 ↔ ( 𝐹 ∈ X 𝑖 ∈ 𝐼 ( 𝑆 ‘ 𝑖 ) ∧ 𝐹 finSupp 0 ) )
23		df-3an	⊢ ( ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ∧ 𝐹 finSupp 0 ) ↔ ( ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ) ∧ 𝐹 finSupp 0 ) )
24	20 22 23	3bitr4g	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑊 ↔ ( 𝐹 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑆 ‘ 𝑥 ) ∧ 𝐹 finSupp 0 ) ) )

Metamath Proof Explorer

Theorem dprdw

Proof