Metamath Proof Explorer

Theorem elpglem3

Description: Lemma for elpg . (Contributed by Emmett Weisz, 28-Aug-2021)

		Ref	Expression
	Assertion	elpglem3	$⊢ \exists x (x \subseteq Pg \land A \in (y \in V ⟼ 𝒫 y \times 𝒫 y) (x)) \leftrightarrow (A \in (V \times V) \land \exists x (x \subseteq Pg \land (1^{st} (A) \in 𝒫 x \land 2^{nd} (A) \in 𝒫 x)))$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2		pweq	$⊢ y = x \to 𝒫 y = 𝒫 x$
3	2	sqxpeqd	$⊢ y = x \to 𝒫 y \times 𝒫 y = 𝒫 x \times 𝒫 x$
4		eqid	$⊢ (y \in V ⟼ 𝒫 y \times 𝒫 y) = (y \in V ⟼ 𝒫 y \times 𝒫 y)$
5	1	pwex	$⊢ 𝒫 x \in V$
6	5 5	xpex	$⊢ 𝒫 x \times 𝒫 x \in V$
7	3 4 6	fvmpt	$⊢ x \in V \to (y \in V ⟼ 𝒫 y \times 𝒫 y) (x) = 𝒫 x \times 𝒫 x$
8	1 7	ax-mp	$⊢ (y \in V ⟼ 𝒫 y \times 𝒫 y) (x) = 𝒫 x \times 𝒫 x$
9	8	eleq2i	$⊢ A \in (y \in V ⟼ 𝒫 y \times 𝒫 y) (x) \leftrightarrow A \in (𝒫 x \times 𝒫 x)$
10		elxp7	$⊢ A \in (𝒫 x \times 𝒫 x) \leftrightarrow (A \in (V \times V) \land (1^{st} (A) \in 𝒫 x \land 2^{nd} (A) \in 𝒫 x))$
11	9 10	bitri	$⊢ A \in (y \in V ⟼ 𝒫 y \times 𝒫 y) (x) \leftrightarrow (A \in (V \times V) \land (1^{st} (A) \in 𝒫 x \land 2^{nd} (A) \in 𝒫 x))$
12	11	anbi2i	$⊢ (x \subseteq Pg \land A \in (y \in V ⟼ 𝒫 y \times 𝒫 y) (x)) \leftrightarrow (x \subseteq Pg \land (A \in (V \times V) \land (1^{st} (A) \in 𝒫 x \land 2^{nd} (A) \in 𝒫 x)))$
13		an12	$⊢ (x \subseteq Pg \land (A \in (V \times V) \land (1^{st} (A) \in 𝒫 x \land 2^{nd} (A) \in 𝒫 x))) \leftrightarrow (A \in (V \times V) \land (x \subseteq Pg \land (1^{st} (A) \in 𝒫 x \land 2^{nd} (A) \in 𝒫 x)))$
14	12 13	bitri	$⊢ (x \subseteq Pg \land A \in (y \in V ⟼ 𝒫 y \times 𝒫 y) (x)) \leftrightarrow (A \in (V \times V) \land (x \subseteq Pg \land (1^{st} (A) \in 𝒫 x \land 2^{nd} (A) \in 𝒫 x)))$
15	14	exbii	$⊢ \exists x (x \subseteq Pg \land A \in (y \in V ⟼ 𝒫 y \times 𝒫 y) (x)) \leftrightarrow \exists x (A \in (V \times V) \land (x \subseteq Pg \land (1^{st} (A) \in 𝒫 x \land 2^{nd} (A) \in 𝒫 x)))$
16		19.42v	$⊢ \exists x (A \in (V \times V) \land (x \subseteq Pg \land (1^{st} (A) \in 𝒫 x \land 2^{nd} (A) \in 𝒫 x))) \leftrightarrow (A \in (V \times V) \land \exists x (x \subseteq Pg \land (1^{st} (A) \in 𝒫 x \land 2^{nd} (A) \in 𝒫 x)))$
17	15 16	bitri	$⊢ \exists x (x \subseteq Pg \land A \in (y \in V ⟼ 𝒫 y \times 𝒫 y) (x)) \leftrightarrow (A \in (V \times V) \land \exists x (x \subseteq Pg \land (1^{st} (A) \in 𝒫 x \land 2^{nd} (A) \in 𝒫 x)))$