bj-imdirval2lem

	Ref	Expression
Hypotheses	bj-imdirval2lem.exa	$⊢ φ \to A \in U$
	bj-imdirval2lem.exb	$⊢ φ \to B \in V$
Assertion	bj-imdirval2lem	$⊢ φ \to \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq B) \land ψ)\} \in V$

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

Metamath Proof Explorer