Theorem elpglem2

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

	Ref	Expression
Assertion	elpglem2	$$⊢\left(1^{st}\left(A\right)\subseteq \mathrm{Pg}\wedge 2^{nd}\left(A\right)\subseteq \mathrm{Pg}\right)\to \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)$$

Proof

Step	Hyp	Ref	Expression
1		fvex	$$⊢1^{st}\left(A\right)\in \mathrm{V}$$
2		fvex	$$⊢2^{nd}\left(A\right)\in \mathrm{V}$$
3	1 2	unex	$$⊢1^{st}\left(A\right)\cup 2^{nd}\left(A\right)\in \mathrm{V}$$
4	3	isseti	$$⊢\exists xx=1^{st}\left(A\right)\cup 2^{nd}\left(A\right)$$
5		sseq1	$$⊢x=1^{st}\left(A\right)\cup 2^{nd}\left(A\right)\to \left(x\subseteq \mathrm{Pg}\leftrightarrow 1^{st}\left(A\right)\cup 2^{nd}\left(A\right)\subseteq \mathrm{Pg}\right)$$
6		unss	$$⊢\left(1^{st}\left(A\right)\subseteq \mathrm{Pg}\wedge 2^{nd}\left(A\right)\subseteq \mathrm{Pg}\right)\leftrightarrow 1^{st}\left(A\right)\cup 2^{nd}\left(A\right)\subseteq \mathrm{Pg}$$
7	5 6	bitr4di	$$⊢x=1^{st}\left(A\right)\cup 2^{nd}\left(A\right)\to \left(x\subseteq \mathrm{Pg}\leftrightarrow \left(1^{st}\left(A\right)\subseteq \mathrm{Pg}\wedge 2^{nd}\left(A\right)\subseteq \mathrm{Pg}\right)\right)$$
8	7	biimprd	$$⊢x=1^{st}\left(A\right)\cup 2^{nd}\left(A\right)\to \left(\left(1^{st}\left(A\right)\subseteq \mathrm{Pg}\wedge 2^{nd}\left(A\right)\subseteq \mathrm{Pg}\right)\to x\subseteq \mathrm{Pg}\right)$$
9		ssun1	$$⊢1^{st}\left(A\right)\subseteq 1^{st}\left(A\right)\cup 2^{nd}\left(A\right)$$
10		id	$$⊢x=1^{st}\left(A\right)\cup 2^{nd}\left(A\right)\to x=1^{st}\left(A\right)\cup 2^{nd}\left(A\right)$$
11	9 10	sseqtrrid	$$⊢x=1^{st}\left(A\right)\cup 2^{nd}\left(A\right)\to 1^{st}\left(A\right)\subseteq x$$
12		vex	$$⊢x\in \mathrm{V}$$
13	12	elpw2	$$⊢1^{st}\left(A\right)\in 𝒫x\leftrightarrow 1^{st}\left(A\right)\subseteq x$$
14	11 13	sylibr	$$⊢x=1^{st}\left(A\right)\cup 2^{nd}\left(A\right)\to 1^{st}\left(A\right)\in 𝒫x$$
15		ssun2	$$⊢2^{nd}\left(A\right)\subseteq 1^{st}\left(A\right)\cup 2^{nd}\left(A\right)$$
16	15 10	sseqtrrid	$$⊢x=1^{st}\left(A\right)\cup 2^{nd}\left(A\right)\to 2^{nd}\left(A\right)\subseteq x$$
17	12	elpw2	$$⊢2^{nd}\left(A\right)\in 𝒫x\leftrightarrow 2^{nd}\left(A\right)\subseteq x$$
18	16 17	sylibr	$$⊢x=1^{st}\left(A\right)\cup 2^{nd}\left(A\right)\to 2^{nd}\left(A\right)\in 𝒫x$$
19	14 18	jca	$$⊢x=1^{st}\left(A\right)\cup 2^{nd}\left(A\right)\to \left(1^{st}\left(A\right)\in 𝒫x\wedge 2^{nd}\left(A\right)\in 𝒫x\right)$$
20	8 19	jctird	$$⊢x=1^{st}\left(A\right)\cup 2^{nd}\left(A\right)\to \left(\left(1^{st}\left(A\right)\subseteq \mathrm{Pg}\wedge 2^{nd}\left(A\right)\subseteq \mathrm{Pg}\right)\to \left(x\subseteq \mathrm{Pg}\wedge \left(1^{st}\left(A\right)\in 𝒫x\wedge 2^{nd}\left(A\right)\in 𝒫x\right)\right)\right)$$
21	4 20	eximii	$$⊢\exists x\left(\left(1^{st}\left(A\right)\subseteq \mathrm{Pg}\wedge 2^{nd}\left(A\right)\subseteq \mathrm{Pg}\right)\to \left(x\subseteq \mathrm{Pg}\wedge \left(1^{st}\left(A\right)\in 𝒫x\wedge 2^{nd}\left(A\right)\in 𝒫x\right)\right)\right)$$
22	21	19.37iv	$$⊢\left(1^{st}\left(A\right)\subseteq \mathrm{Pg}\wedge 2^{nd}\left(A\right)\subseteq \mathrm{Pg}\right)\to \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)$$