Theorem bj-imdirval2lem

Description: Lemma for bj-imdirval2 and bj-iminvval2 . (Contributed by BJ, 23-May-2024)

	Ref	Expression
Hypotheses	bj-imdirval2lem.exa	|- ( ph -> A e. U )
	bj-imdirval2lem.exb	|- ( ph -> B e. V )
Assertion	bj-imdirval2lem	|- ( ph -> { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ps ) } e. _V )

Proof

Step	Hyp	Ref	Expression
1		bj-imdirval2lem.exa	|- ( ph -> A e. U )
2		bj-imdirval2lem.exb	|- ( ph -> B e. V )
3	1	pwexd	|- ( ph -> ~P A e. _V )
4	2	pwexd	|- ( ph -> ~P B e. _V )
5		simprl	|- ( ( ph /\ ( x C_ A /\ y C_ B ) ) -> x C_ A )
6		velpw	|- ( x e. ~P A <-> x C_ A )
7	5 6	sylibr	|- ( ( ph /\ ( x C_ A /\ y C_ B ) ) -> x e. ~P A )
8		simprr	|- ( ( ph /\ ( x C_ A /\ y C_ B ) ) -> y C_ B )
9		velpw	|- ( y e. ~P B <-> y C_ B )
10	8 9	sylibr	|- ( ( ph /\ ( x C_ A /\ y C_ B ) ) -> y e. ~P B )
11	3 4 7 10	opabex2	|- ( ph -> { <. x , y >. | ( x C_ A /\ y C_ B ) } e. _V )
12		simpl	|- ( ( ( x C_ A /\ y C_ B ) /\ ps ) -> ( x C_ A /\ y C_ B ) )
13	12	ssopab2i	|- { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ps ) } C_ { <. x , y >. | ( x C_ A /\ y C_ B ) }
14	13	a1i	|- ( ph -> { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ps ) } C_ { <. x , y >. | ( x C_ A /\ y C_ B ) } )
15	11 14	ssexd	|- ( ph -> { <. x , y >. | ( ( x C_ A /\ y C_ B ) /\ ps ) } e. _V )