This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pwselbasr

Description: The reverse direction of pwselbasb : a function between the index and base set of a structure is an element of the structure power. (Contributed by SN, 29-Jul-2024)

Ref Expression
Hypotheses pwsbas.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
pwsbas.f ⊢ 𝐵 = ( Base ‘ 𝑅 )
pwselbas.v ⊢ 𝑉 = ( Base ‘ 𝑌 )
pwselbas.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
pwselbas.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑍 )
pwselbasr.x ⊢ ( 𝜑 → 𝑋 : 𝐼 ⟶ 𝐵 )
Assertion pwselbasr ( 𝜑 → 𝑋 ∈ 𝑉 )

Proof

Step Hyp Ref Expression
1 pwsbas.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2 pwsbas.f ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 pwselbas.v ⊢ 𝑉 = ( Base ‘ 𝑌 )
4 pwselbas.r ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 )
5 pwselbas.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑍 )
6 pwselbasr.x ⊢ ( 𝜑 → 𝑋 : 𝐼 ⟶ 𝐵 )
7 1 2 3 pwselbasb ⊢ ( ( 𝑅 ∈ 𝑊 ∧ 𝐼 ∈ 𝑍 ) → ( 𝑋 ∈ 𝑉 ↔ 𝑋 : 𝐼 ⟶ 𝐵 ) )
8 4 5 7 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑉 ↔ 𝑋 : 𝐼 ⟶ 𝐵 ) )
9 6 8 mpbird ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )