Theorem pgindlem

Description: Lemma for pgind . (Contributed by Emmett Weisz, 27-May-2024) (New usage is discouraged.)

	Ref	Expression
Assertion	pgindlem	$$⊢x\in \left(𝒫z\times 𝒫z\right)\to 1^{st}\left(x\right)\cup 2^{nd}\left(x\right)\subseteq z$$

Proof

Step	Hyp	Ref	Expression
1		xp1st	$$⊢x\in \left(𝒫z\times 𝒫z\right)\to 1^{st}\left(x\right)\in 𝒫z$$
2	1	elpwid	$$⊢x\in \left(𝒫z\times 𝒫z\right)\to 1^{st}\left(x\right)\subseteq z$$
3		xp2nd	$$⊢x\in \left(𝒫z\times 𝒫z\right)\to 2^{nd}\left(x\right)\in 𝒫z$$
4	3	elpwid	$$⊢x\in \left(𝒫z\times 𝒫z\right)\to 2^{nd}\left(x\right)\subseteq z$$
5	2 4	unssd	$$⊢x\in \left(𝒫z\times 𝒫z\right)\to 1^{st}\left(x\right)\cup 2^{nd}\left(x\right)\subseteq z$$