Theorem elpglem1

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

	Ref	Expression
Assertion	elpglem1	$$⊢\exists x\left(x\subseteq \mathrm{Pg}\wedge \left(1^{st}\left(A\right)\in 𝒫x\wedge 2^{nd}\left(A\right)\in 𝒫x\right)\right)\to \left(1^{st}\left(A\right)\subseteq \mathrm{Pg}\wedge 2^{nd}\left(A\right)\subseteq \mathrm{Pg}\right)$$

Proof

Step	Hyp	Ref	Expression
1		elpwi	$$⊢1^{st}\left(A\right)\in 𝒫x\to 1^{st}\left(A\right)\subseteq x$$
2	1	adantl	$$⊢\left(x\subseteq \mathrm{Pg}\wedge 1^{st}\left(A\right)\in 𝒫x\right)\to 1^{st}\left(A\right)\subseteq x$$
3		simpl	$$⊢\left(x\subseteq \mathrm{Pg}\wedge 1^{st}\left(A\right)\in 𝒫x\right)\to x\subseteq \mathrm{Pg}$$
4	2 3	sstrd	$$⊢\left(x\subseteq \mathrm{Pg}\wedge 1^{st}\left(A\right)\in 𝒫x\right)\to 1^{st}\left(A\right)\subseteq \mathrm{Pg}$$
5		elpwi	$$⊢2^{nd}\left(A\right)\in 𝒫x\to 2^{nd}\left(A\right)\subseteq x$$
6	5	adantl	$$⊢\left(x\subseteq \mathrm{Pg}\wedge 2^{nd}\left(A\right)\in 𝒫x\right)\to 2^{nd}\left(A\right)\subseteq x$$
7		simpl	$$⊢\left(x\subseteq \mathrm{Pg}\wedge 2^{nd}\left(A\right)\in 𝒫x\right)\to x\subseteq \mathrm{Pg}$$
8	6 7	sstrd	$$⊢\left(x\subseteq \mathrm{Pg}\wedge 2^{nd}\left(A\right)\in 𝒫x\right)\to 2^{nd}\left(A\right)\subseteq \mathrm{Pg}$$
9	4 8	anim12dan	$$⊢\left(x\subseteq \mathrm{Pg}\wedge \left(1^{st}\left(A\right)\in 𝒫x\wedge 2^{nd}\left(A\right)\in 𝒫x\right)\right)\to \left(1^{st}\left(A\right)\subseteq \mathrm{Pg}\wedge 2^{nd}\left(A\right)\subseteq \mathrm{Pg}\right)$$
10	9	exlimiv	$$⊢\exists x\left(x\subseteq \mathrm{Pg}\wedge \left(1^{st}\left(A\right)\in 𝒫x\wedge 2^{nd}\left(A\right)\in 𝒫x\right)\right)\to \left(1^{st}\left(A\right)\subseteq \mathrm{Pg}\wedge 2^{nd}\left(A\right)\subseteq \mathrm{Pg}\right)$$