Theorem pwselbasb

Description: Membership in the base set of a structure product. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Hypotheses	pwsbas.y	⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
	pwsbas.f	⊢ 𝐵 = ( Base ‘ 𝑅 )
	pwselbas.v	⊢ 𝑉 = ( Base ‘ 𝑌 )
Assertion	pwselbasb	⊢ ( ( 𝑅 ∈ 𝑊 ∧ 𝐼 ∈ 𝑍 ) → ( 𝑋 ∈ 𝑉 ↔ 𝑋 : 𝐼 ⟶ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		pwsbas.y	⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2		pwsbas.f	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		pwselbas.v	⊢ 𝑉 = ( Base ‘ 𝑌 )
4	1 2	pwsbas	⊢ ( ( 𝑅 ∈ 𝑊 ∧ 𝐼 ∈ 𝑍 ) → ( 𝐵 ↑m 𝐼 ) = ( Base ‘ 𝑌 ) )
5	4 3	eqtr4di	⊢ ( ( 𝑅 ∈ 𝑊 ∧ 𝐼 ∈ 𝑍 ) → ( 𝐵 ↑m 𝐼 ) = 𝑉 )
6	5	eleq2d	⊢ ( ( 𝑅 ∈ 𝑊 ∧ 𝐼 ∈ 𝑍 ) → ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ↔ 𝑋 ∈ 𝑉 ) )
7	2	fvexi	⊢ 𝐵 ∈ V
8		elmapg	⊢ ( ( 𝐵 ∈ V ∧ 𝐼 ∈ 𝑍 ) → ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ↔ 𝑋 : 𝐼 ⟶ 𝐵 ) )
9	7 8	mpan	⊢ ( 𝐼 ∈ 𝑍 → ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ↔ 𝑋 : 𝐼 ⟶ 𝐵 ) )
10	9	adantl	⊢ ( ( 𝑅 ∈ 𝑊 ∧ 𝐼 ∈ 𝑍 ) → ( 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ↔ 𝑋 : 𝐼 ⟶ 𝐵 ) )
11	6 10	bitr3d	⊢ ( ( 𝑅 ∈ 𝑊 ∧ 𝐼 ∈ 𝑍 ) → ( 𝑋 ∈ 𝑉 ↔ 𝑋 : 𝐼 ⟶ 𝐵 ) )