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 \in V \land I \in W) \land A \in B) \to I \times \{A\} \in C$

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 \in B \to (I \times \{A\}) : I ⟶ B$
5	4	adantl	$⊢ ((R \in V \land I \in W) \land A \in B) \to (I \times \{A\}) : I ⟶ B$
6	1 2 3	pwselbasb	$⊢ (R \in V \land I \in W) \to (I \times \{A\} \in C \leftrightarrow (I \times \{A\}) : I ⟶ B)$
7	6	adantr	$⊢ ((R \in V \land I \in W) \land A \in B) \to (I \times \{A\} \in C \leftrightarrow (I \times \{A\}) : I ⟶ B)$
8	5 7	mpbird	$⊢ ((R \in V \land I \in W) \land A \in B) \to I \times \{A\} \in C$

Metamath Proof Explorer