Metamath Proof Explorer


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 Y = R 𝑠 I
pwsdiagel.b B = Base R
pwsdiagel.c C = Base Y
Assertion pwsdiagel R V I W A B I × A C

Proof

Step Hyp Ref Expression
1 pwsdiagel.y Y = R 𝑠 I
2 pwsdiagel.b B = Base R
3 pwsdiagel.c C = Base Y
4 fconst6g A B I × A : I B
5 4 adantl R V I W A B I × A : I B
6 1 2 3 pwselbasb R V I W I × A C I × A : I B
7 6 adantr R V I W A B I × A C I × A : I B
8 5 7 mpbird R V I W A B I × A C