Theorem pwsdiagel

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

	Ref	Expression
Hypotheses	pwsdiagel.y	⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
	pwsdiagel.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	pwsdiagel.c	⊢ 𝐶 = ( Base ‘ 𝑌 )
Assertion	pwsdiagel	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐼 × { 𝐴 } ) ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		pwsdiagel.y	⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2		pwsdiagel.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		pwsdiagel.c	⊢ 𝐶 = ( Base ‘ 𝑌 )
4		fconst6g	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐼 × { 𝐴 } ) : 𝐼 ⟶ 𝐵 )
5	4	adantl	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐼 × { 𝐴 } ) : 𝐼 ⟶ 𝐵 )
6	1 2 3	pwselbasb	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) → ( ( 𝐼 × { 𝐴 } ) ∈ 𝐶 ↔ ( 𝐼 × { 𝐴 } ) : 𝐼 ⟶ 𝐵 ) )
7	6	adantr	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝐼 × { 𝐴 } ) ∈ 𝐶 ↔ ( 𝐼 × { 𝐴 } ) : 𝐼 ⟶ 𝐵 ) )
8	5 7	mpbird	⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝐼 ∈ 𝑊 ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐼 × { 𝐴 } ) ∈ 𝐶 )