bj-imdirvallem

	Ref	Expression
Hypotheses	bj-imdirvallem.1	$⊢ φ \to A \in U$
	bj-imdirvallem.2	$⊢ φ \to B \in V$
	bj-imdirvallem.df	$⊢ C = (a \in V, b \in V ⟼ (r \in 𝒫 (a \times b) ⟼ \{⟨x, y⟩ \| ((x \subseteq a \land y \subseteq b) \land ψ)\}))$
Assertion	bj-imdirvallem	$⊢ φ \to A C B = (r \in 𝒫 (A \times B) ⟼ \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq B) \land ψ)\})$

Proof

Step	Hyp	Ref	Expression
1		bj-imdirvallem.1	$⊢ φ \to A \in U$
2		bj-imdirvallem.2	$⊢ φ \to B \in V$
3		bj-imdirvallem.df	$⊢ C = (a \in V, b \in V ⟼ (r \in 𝒫 (a \times b) ⟼ \{⟨x, y⟩ \| ((x \subseteq a \land y \subseteq b) \land ψ)\}))$
4	3	a1i	$⊢ φ \to C = (a \in V, b \in V ⟼ (r \in 𝒫 (a \times b) ⟼ \{⟨x, y⟩ \| ((x \subseteq a \land y \subseteq b) \land ψ)\}))$
5		xpeq12	$⊢ (a = A \land b = B) \to a \times b = A \times B$
6	5	pweqd	$⊢ (a = A \land b = B) \to 𝒫 (a \times b) = 𝒫 (A \times B)$
7	6	adantl	$⊢ (φ \land (a = A \land b = B)) \to 𝒫 (a \times b) = 𝒫 (A \times B)$
8		sseq2	$⊢ a = A \to (x \subseteq a \leftrightarrow x \subseteq A)$
9		sseq2	$⊢ b = B \to (y \subseteq b \leftrightarrow y \subseteq B)$
10	8 9	bi2anan9	$⊢ (a = A \land b = B) \to ((x \subseteq a \land y \subseteq b) \leftrightarrow (x \subseteq A \land y \subseteq B))$
11	10	anbi1d	$⊢ (a = A \land b = B) \to (((x \subseteq a \land y \subseteq b) \land ψ) \leftrightarrow ((x \subseteq A \land y \subseteq B) \land ψ))$
12	11	opabbidv	$⊢ (a = A \land b = B) \to \{⟨x, y⟩ \| ((x \subseteq a \land y \subseteq b) \land ψ)\} = \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq B) \land ψ)\}$
13	12	adantl	$⊢ (φ \land (a = A \land b = B)) \to \{⟨x, y⟩ \| ((x \subseteq a \land y \subseteq b) \land ψ)\} = \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq B) \land ψ)\}$
14	7 13	mpteq12dv	$⊢ (φ \land (a = A \land b = B)) \to (r \in 𝒫 (a \times b) ⟼ \{⟨x, y⟩ \| ((x \subseteq a \land y \subseteq b) \land ψ)\}) = (r \in 𝒫 (A \times B) ⟼ \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq B) \land ψ)\})$
15	1	elexd	$⊢ φ \to A \in V$
16	2	elexd	$⊢ φ \to B \in V$
17	1 2	xpexd	$⊢ φ \to A \times B \in V$
18	17	pwexd	$⊢ φ \to 𝒫 (A \times B) \in V$
19	18	mptexd	$⊢ φ \to (r \in 𝒫 (A \times B) ⟼ \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq B) \land ψ)\}) \in V$
20	4 14 15 16 19	ovmpod	$⊢ φ \to A C B = (r \in 𝒫 (A \times B) ⟼ \{⟨x, y⟩ \| ((x \subseteq A \land y \subseteq B) \land ψ)\})$

Metamath Proof Explorer

Theorem bj-imdirvallem

Proof