Theorem pgindlem

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

	Ref	Expression
Assertion	pgindlem	|- ( x e. ( ~P z X. ~P z ) -> ( ( 1st ` x ) u. ( 2nd ` x ) ) C_ z )

Proof

Step	Hyp	Ref	Expression
1		xp1st	|- ( x e. ( ~P z X. ~P z ) -> ( 1st ` x ) e. ~P z )
2	1	elpwid	|- ( x e. ( ~P z X. ~P z ) -> ( 1st ` x ) C_ z )
3		xp2nd	|- ( x e. ( ~P z X. ~P z ) -> ( 2nd ` x ) e. ~P z )
4	3	elpwid	|- ( x e. ( ~P z X. ~P z ) -> ( 2nd ` x ) C_ z )
5	2 4	unssd	|- ( x e. ( ~P z X. ~P z ) -> ( ( 1st ` x ) u. ( 2nd ` x ) ) C_ z )