Metamath Proof Explorer

Theorem elpglem3

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

		Ref	Expression
	Assertion	elpglem3	⊢ ( ∃ 𝑥 ( 𝑥 ⊆ Pg ∧ 𝐴 ∈ ( ( 𝑦 ∈ V ↦ ( 𝒫 𝑦 × 𝒫 𝑦 ) ) ‘ 𝑥 ) ) ↔ ( 𝐴 ∈ ( V × V ) ∧ ∃ 𝑥 ( 𝑥 ⊆ Pg ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2		pweq	⊢ ( 𝑦 = 𝑥 → 𝒫 𝑦 = 𝒫 𝑥 )
3	2	sqxpeqd	⊢ ( 𝑦 = 𝑥 → ( 𝒫 𝑦 × 𝒫 𝑦 ) = ( 𝒫 𝑥 × 𝒫 𝑥 ) )
4		eqid	⊢ ( 𝑦 ∈ V ↦ ( 𝒫 𝑦 × 𝒫 𝑦 ) ) = ( 𝑦 ∈ V ↦ ( 𝒫 𝑦 × 𝒫 𝑦 ) )
5	1	pwex	⊢ 𝒫 𝑥 ∈ V
6	5 5	xpex	⊢ ( 𝒫 𝑥 × 𝒫 𝑥 ) ∈ V
7	3 4 6	fvmpt	⊢ ( 𝑥 ∈ V → ( ( 𝑦 ∈ V ↦ ( 𝒫 𝑦 × 𝒫 𝑦 ) ) ‘ 𝑥 ) = ( 𝒫 𝑥 × 𝒫 𝑥 ) )
8	1 7	ax-mp	⊢ ( ( 𝑦 ∈ V ↦ ( 𝒫 𝑦 × 𝒫 𝑦 ) ) ‘ 𝑥 ) = ( 𝒫 𝑥 × 𝒫 𝑥 )
9	8	eleq2i	⊢ ( 𝐴 ∈ ( ( 𝑦 ∈ V ↦ ( 𝒫 𝑦 × 𝒫 𝑦 ) ) ‘ 𝑥 ) ↔ 𝐴 ∈ ( 𝒫 𝑥 × 𝒫 𝑥 ) )
10		elxp7	⊢ ( 𝐴 ∈ ( 𝒫 𝑥 × 𝒫 𝑥 ) ↔ ( 𝐴 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) ) )
11	9 10	bitri	⊢ ( 𝐴 ∈ ( ( 𝑦 ∈ V ↦ ( 𝒫 𝑦 × 𝒫 𝑦 ) ) ‘ 𝑥 ) ↔ ( 𝐴 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) ) )
12	11	anbi2i	⊢ ( ( 𝑥 ⊆ Pg ∧ 𝐴 ∈ ( ( 𝑦 ∈ V ↦ ( 𝒫 𝑦 × 𝒫 𝑦 ) ) ‘ 𝑥 ) ) ↔ ( 𝑥 ⊆ Pg ∧ ( 𝐴 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) ) ) )
13		an12	⊢ ( ( 𝑥 ⊆ Pg ∧ ( 𝐴 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) ) ) ↔ ( 𝐴 ∈ ( V × V ) ∧ ( 𝑥 ⊆ Pg ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) ) ) )
14	12 13	bitri	⊢ ( ( 𝑥 ⊆ Pg ∧ 𝐴 ∈ ( ( 𝑦 ∈ V ↦ ( 𝒫 𝑦 × 𝒫 𝑦 ) ) ‘ 𝑥 ) ) ↔ ( 𝐴 ∈ ( V × V ) ∧ ( 𝑥 ⊆ Pg ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) ) ) )
15	14	exbii	⊢ ( ∃ 𝑥 ( 𝑥 ⊆ Pg ∧ 𝐴 ∈ ( ( 𝑦 ∈ V ↦ ( 𝒫 𝑦 × 𝒫 𝑦 ) ) ‘ 𝑥 ) ) ↔ ∃ 𝑥 ( 𝐴 ∈ ( V × V ) ∧ ( 𝑥 ⊆ Pg ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) ) ) )
16		19.42v	⊢ ( ∃ 𝑥 ( 𝐴 ∈ ( V × V ) ∧ ( 𝑥 ⊆ Pg ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) ) ) ↔ ( 𝐴 ∈ ( V × V ) ∧ ∃ 𝑥 ( 𝑥 ⊆ Pg ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) ) ) )
17	15 16	bitri	⊢ ( ∃ 𝑥 ( 𝑥 ⊆ Pg ∧ 𝐴 ∈ ( ( 𝑦 ∈ V ↦ ( 𝒫 𝑦 × 𝒫 𝑦 ) ) ‘ 𝑥 ) ) ↔ ( 𝐴 ∈ ( V × V ) ∧ ∃ 𝑥 ( 𝑥 ⊆ Pg ∧ ( ( 1^st ‘ 𝐴 ) ∈ 𝒫 𝑥 ∧ ( 2^nd ‘ 𝐴 ) ∈ 𝒫 𝑥 ) ) ) )