Theorem prdsbascl

Description: An element of the base has projections closed in the factors. (Contributed by Mario Carneiro, 27-Aug-2015)

	Ref	Expression
Hypotheses	prdsbasmpt2.y	⊢ 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
	prdsbasmpt2.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	prdsbasmpt2.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	prdsbasmpt2.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	prdsbasmpt2.r	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑋 )
	prdsbasmpt2.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	prdsbascl.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion	prdsbascl	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt2.y	⊢ 𝑌 = ( 𝑆 Xs ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) )
2		prdsbasmpt2.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
3		prdsbasmpt2.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
4		prdsbasmpt2.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5		prdsbasmpt2.r	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑋 )
6		prdsbasmpt2.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
7		prdsbascl.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
8		eqid	⊢ ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) = ( 𝑥 ∈ 𝐼 ↦ 𝑅 )
9	8	fnmpt	⊢ ( ∀ 𝑥 ∈ 𝐼 𝑅 ∈ 𝑋 → ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) Fn 𝐼 )
10	5 9	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝑅 ) Fn 𝐼 )
11	1 2 3 4 10 7	prdsbasfn	⊢ ( 𝜑 → 𝐹 Fn 𝐼 )
12		dffn5	⊢ ( 𝐹 Fn 𝐼 ↔ 𝐹 = ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑥 ) ) )
13	11 12	sylib	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑥 ) ) )
14	13 7	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐵 )
15	1 2 3 4 5 6	prdsbasmpt2	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ 𝐾 ) )
16	14 15	mpbid	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( 𝐹 ‘ 𝑥 ) ∈ 𝐾 )