Theorem pgindlem

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

	Ref	Expression
Assertion	pgindlem	⊢ ( 𝑥 ∈ ( 𝒫 𝑧 × 𝒫 𝑧 ) → ( ( 1st ‘ 𝑥 ) ∪ ( 2nd ‘ 𝑥 ) ) ⊆ 𝑧 )

Proof

Step	Hyp	Ref	Expression
1		xp1st	⊢ ( 𝑥 ∈ ( 𝒫 𝑧 × 𝒫 𝑧 ) → ( 1st ‘ 𝑥 ) ∈ 𝒫 𝑧 )
2	1	elpwid	⊢ ( 𝑥 ∈ ( 𝒫 𝑧 × 𝒫 𝑧 ) → ( 1st ‘ 𝑥 ) ⊆ 𝑧 )
3		xp2nd	⊢ ( 𝑥 ∈ ( 𝒫 𝑧 × 𝒫 𝑧 ) → ( 2nd ‘ 𝑥 ) ∈ 𝒫 𝑧 )
4	3	elpwid	⊢ ( 𝑥 ∈ ( 𝒫 𝑧 × 𝒫 𝑧 ) → ( 2nd ‘ 𝑥 ) ⊆ 𝑧 )
5	2 4	unssd	⊢ ( 𝑥 ∈ ( 𝒫 𝑧 × 𝒫 𝑧 ) → ( ( 1st ‘ 𝑥 ) ∪ ( 2nd ‘ 𝑥 ) ) ⊆ 𝑧 )