Theorem bj-imdirval2lem

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

	Ref	Expression
Hypotheses	bj-imdirval2lem.exa	$$⊢\phi \to A\in U$$
	bj-imdirval2lem.exb	$$⊢\phi \to B\in V$$
Assertion	bj-imdirval2lem	$$⊢\phi \to \left\{⟨x,y⟩|\left(\left(x\subseteq A\wedge y\subseteq B\right)\wedge \psi \right)\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		bj-imdirval2lem.exa	$$⊢\phi \to A\in U$$
2		bj-imdirval2lem.exb	$$⊢\phi \to B\in V$$
3	1	pwexd	$$⊢\phi \to 𝒫A\in \mathrm{V}$$
4	2	pwexd	$$⊢\phi \to 𝒫B\in \mathrm{V}$$
5		simprl	$$⊢\left(\phi \wedge \left(x\subseteq A\wedge y\subseteq B\right)\right)\to x\subseteq A$$
6		velpw	$$⊢x\in 𝒫A\leftrightarrow x\subseteq A$$
7	5 6	sylibr	$$⊢\left(\phi \wedge \left(x\subseteq A\wedge y\subseteq B\right)\right)\to x\in 𝒫A$$
8		simprr	$$⊢\left(\phi \wedge \left(x\subseteq A\wedge y\subseteq B\right)\right)\to y\subseteq B$$
9		velpw	$$⊢y\in 𝒫B\leftrightarrow y\subseteq B$$
10	8 9	sylibr	$$⊢\left(\phi \wedge \left(x\subseteq A\wedge y\subseteq B\right)\right)\to y\in 𝒫B$$
11	3 4 7 10	opabex2	$$⊢\phi \to \left\{⟨x,y⟩|\left(x\subseteq A\wedge y\subseteq B\right)\right\}\in \mathrm{V}$$
12		simpl	$$⊢\left(\left(x\subseteq A\wedge y\subseteq B\right)\wedge \psi \right)\to \left(x\subseteq A\wedge y\subseteq B\right)$$
13	12	ssopab2i	$$⊢\left\{⟨x,y⟩|\left(\left(x\subseteq A\wedge y\subseteq B\right)\wedge \psi \right)\right\}\subseteq \left\{⟨x,y⟩|\left(x\subseteq A\wedge y\subseteq B\right)\right\}$$
14	13	a1i	$$⊢\phi \to \left\{⟨x,y⟩|\left(\left(x\subseteq A\wedge y\subseteq B\right)\wedge \psi \right)\right\}\subseteq \left\{⟨x,y⟩|\left(x\subseteq A\wedge y\subseteq B\right)\right\}$$
15	11 14	ssexd	$$⊢\phi \to \left\{⟨x,y⟩|\left(\left(x\subseteq A\wedge y\subseteq B\right)\wedge \psi \right)\right\}\in \mathrm{V}$$