xpab

Description: Cartesian product of two class abstractions. (Contributed by Scott Fenton, 19-Aug-2024)

		Ref	Expression
	Assertion	xpab	$⊢ \{x \| φ\} \times \{y \| ψ\} = \{⟨x, y⟩ \| (φ \land ψ)\}$

Proof

Step	Hyp	Ref	Expression
1		relxp	$⊢ Rel (\{x \| φ\} \times \{y \| ψ\})$
2		relopabv	$⊢ Rel \{⟨x, y⟩ \| (φ \land ψ)\}$
3		df-clab	$⊢ a \in \{x \| φ\} \leftrightarrow [a/ x] φ$
4		df-clab	$⊢ b \in \{y \| ψ\} \leftrightarrow [b/ y] ψ$
5	3 4	anbi12i	$⊢ (a \in \{x \| φ\} \land b \in \{y \| ψ\}) \leftrightarrow ([a/ x] φ \land [b/ y] ψ)$
6		sban	$⊢ [b/ y] (φ \land ψ) \leftrightarrow ([b/ y] φ \land [b/ y] ψ)$
7		sbsbc	$⊢ [b/ y] (φ \land ψ) \leftrightarrow \underset{˙}{[} b / y \underset{˙}{]} (φ \land ψ)$
8		sbv	$⊢ [b/ y] φ \leftrightarrow φ$
9	8	anbi1i	$⊢ ([b/ y] φ \land [b/ y] ψ) \leftrightarrow (φ \land [b/ y] ψ)$
10	6 7 9	3bitr3i	$⊢ \underset{˙}{[} b / y \underset{˙}{]} (φ \land ψ) \leftrightarrow (φ \land [b/ y] ψ)$
11	10	sbbii	$⊢ [a/ x] \underset{˙}{[} b / y \underset{˙}{]} (φ \land ψ) \leftrightarrow [a/ x] (φ \land [b/ y] ψ)$
12		sbsbc	$⊢ [a/ x] \underset{˙}{[} b / y \underset{˙}{]} (φ \land ψ) \leftrightarrow \underset{˙}{[} a / x \underset{˙}{]} \underset{˙}{[} b / y \underset{˙}{]} (φ \land ψ)$
13		sban	$⊢ [a/ x] (φ \land [b/ y] ψ) \leftrightarrow ([a/ x] φ \land [a/ x] [b/ y] ψ)$
14		sbv	$⊢ [a/ x] [b/ y] ψ \leftrightarrow [b/ y] ψ$
15	14	anbi2i	$⊢ ([a/ x] φ \land [a/ x] [b/ y] ψ) \leftrightarrow ([a/ x] φ \land [b/ y] ψ)$
16	13 15	bitri	$⊢ [a/ x] (φ \land [b/ y] ψ) \leftrightarrow ([a/ x] φ \land [b/ y] ψ)$
17	11 12 16	3bitr3i	$⊢ \underset{˙}{[} a / x \underset{˙}{]} \underset{˙}{[} b / y \underset{˙}{]} (φ \land ψ) \leftrightarrow ([a/ x] φ \land [b/ y] ψ)$
18	5 17	bitr4i	$⊢ (a \in \{x \| φ\} \land b \in \{y \| ψ\}) \leftrightarrow \underset{˙}{[} a / x \underset{˙}{]} \underset{˙}{[} b / y \underset{˙}{]} (φ \land ψ)$
19		brxp	$⊢ a (\{x \| φ\} \times \{y \| ψ\}) b \leftrightarrow (a \in \{x \| φ\} \land b \in \{y \| ψ\})$
20		eqid	$⊢ \{⟨x, y⟩ \| (φ \land ψ)\} = \{⟨x, y⟩ \| (φ \land ψ)\}$
21	20	brabsb	$⊢ a \{⟨x, y⟩ \| (φ \land ψ)\} b \leftrightarrow \underset{˙}{[} a / x \underset{˙}{]} \underset{˙}{[} b / y \underset{˙}{]} (φ \land ψ)$
22	18 19 21	3bitr4i	$⊢ a (\{x \| φ\} \times \{y \| ψ\}) b \leftrightarrow a \{⟨x, y⟩ \| (φ \land ψ)\} b$
23	1 2 22	eqbrriv	$⊢ \{x \| φ\} \times \{y \| ψ\} = \{⟨x, y⟩ \| (φ \land ψ)\}$

Metamath Proof Explorer

Theorem xpab

Proof