bj-opabco

Description: Composition of ordered-pair class abstractions. (Contributed by BJ, 22-May-2024)

		Ref	Expression
	Assertion	bj-opabco	$⊢ \{⟨y, z⟩ \| ψ\} \circ \{⟨x, y⟩ \| φ\} = \{⟨x, z⟩ \| \exists y (φ \land ψ)\}$

Proof

Step	Hyp	Ref	Expression
1		df-co	$⊢ \{⟨y, z⟩ \| ψ\} \circ \{⟨x, y⟩ \| φ\} = \{⟨a, b⟩ \| \exists c (a \{⟨x, y⟩ \| φ\} c \land c \{⟨y, z⟩ \| ψ\} b)\}$
2		nfcv	$⊢ \underline{Ⅎ} x a$
3		nfopab1	$⊢ \underline{Ⅎ} x \{⟨x, y⟩ \| φ\}$
4		nfcv	$⊢ \underline{Ⅎ} x c$
5	2 3 4	nfbr	$⊢ Ⅎ x a \{⟨x, y⟩ \| φ\} c$
6		nfv	$⊢ Ⅎ x c \{⟨y, z⟩ \| ψ\} b$
7	5 6	nfan	$⊢ Ⅎ x (a \{⟨x, y⟩ \| φ\} c \land c \{⟨y, z⟩ \| ψ\} b)$
8	7	nfex	$⊢ Ⅎ x \exists c (a \{⟨x, y⟩ \| φ\} c \land c \{⟨y, z⟩ \| ψ\} b)$
9		nfv	$⊢ Ⅎ z a \{⟨x, y⟩ \| φ\} c$
10		nfcv	$⊢ \underline{Ⅎ} z c$
11		nfopab2	$⊢ \underline{Ⅎ} z \{⟨y, z⟩ \| ψ\}$
12		nfcv	$⊢ \underline{Ⅎ} z b$
13	10 11 12	nfbr	$⊢ Ⅎ z c \{⟨y, z⟩ \| ψ\} b$
14	9 13	nfan	$⊢ Ⅎ z (a \{⟨x, y⟩ \| φ\} c \land c \{⟨y, z⟩ \| ψ\} b)$
15	14	nfex	$⊢ Ⅎ z \exists c (a \{⟨x, y⟩ \| φ\} c \land c \{⟨y, z⟩ \| ψ\} b)$
16		nfv	$⊢ Ⅎ a \exists y (x \{⟨x, y⟩ \| φ\} y \land y \{⟨y, z⟩ \| ψ\} z)$
17		nfv	$⊢ Ⅎ b \exists y (x \{⟨x, y⟩ \| φ\} y \land y \{⟨y, z⟩ \| ψ\} z)$
18		nfv	$⊢ Ⅎ y (a = x \land b = z)$
19		nfcv	$⊢ \underline{Ⅎ} y a$
20		nfopab2	$⊢ \underline{Ⅎ} y \{⟨x, y⟩ \| φ\}$
21		nfcv	$⊢ \underline{Ⅎ} y c$
22	19 20 21	nfbr	$⊢ Ⅎ y a \{⟨x, y⟩ \| φ\} c$
23		nfopab1	$⊢ \underline{Ⅎ} y \{⟨y, z⟩ \| ψ\}$
24		nfcv	$⊢ \underline{Ⅎ} y b$
25	21 23 24	nfbr	$⊢ Ⅎ y c \{⟨y, z⟩ \| ψ\} b$
26	22 25	nfan	$⊢ Ⅎ y (a \{⟨x, y⟩ \| φ\} c \land c \{⟨y, z⟩ \| ψ\} b)$
27	26	a1i	$⊢ (a = x \land b = z) \to Ⅎ y (a \{⟨x, y⟩ \| φ\} c \land c \{⟨y, z⟩ \| ψ\} b)$
28		simpll	$⊢ ((a = x \land b = z) \land c = y) \to a = x$
29		simpr	$⊢ ((a = x \land b = z) \land c = y) \to c = y$
30	28 29	breq12d	$⊢ ((a = x \land b = z) \land c = y) \to (a \{⟨x, y⟩ \| φ\} c \leftrightarrow x \{⟨x, y⟩ \| φ\} y)$
31		simplr	$⊢ ((a = x \land b = z) \land c = y) \to b = z$
32	29 31	breq12d	$⊢ ((a = x \land b = z) \land c = y) \to (c \{⟨y, z⟩ \| ψ\} b \leftrightarrow y \{⟨y, z⟩ \| ψ\} z)$
33	30 32	anbi12d	$⊢ ((a = x \land b = z) \land c = y) \to ((a \{⟨x, y⟩ \| φ\} c \land c \{⟨y, z⟩ \| ψ\} b) \leftrightarrow (x \{⟨x, y⟩ \| φ\} y \land y \{⟨y, z⟩ \| ψ\} z))$
34	33	ex	$⊢ (a = x \land b = z) \to (c = y \to ((a \{⟨x, y⟩ \| φ\} c \land c \{⟨y, z⟩ \| ψ\} b) \leftrightarrow (x \{⟨x, y⟩ \| φ\} y \land y \{⟨y, z⟩ \| ψ\} z)))$
35	18 27 34	cbvexdw	$⊢ (a = x \land b = z) \to (\exists c (a \{⟨x, y⟩ \| φ\} c \land c \{⟨y, z⟩ \| ψ\} b) \leftrightarrow \exists y (x \{⟨x, y⟩ \| φ\} y \land y \{⟨y, z⟩ \| ψ\} z))$
36	8 15 16 17 35	cbvopab	$⊢ \{⟨a, b⟩ \| \exists c (a \{⟨x, y⟩ \| φ\} c \land c \{⟨y, z⟩ \| ψ\} b)\} = \{⟨x, z⟩ \| \exists y (x \{⟨x, y⟩ \| φ\} y \land y \{⟨y, z⟩ \| ψ\} z)\}$
37		bj-opelopabid	$⊢ x \{⟨x, y⟩ \| φ\} y \leftrightarrow φ$
38		bj-opelopabid	$⊢ y \{⟨y, z⟩ \| ψ\} z \leftrightarrow ψ$
39	37 38	anbi12i	$⊢ (x \{⟨x, y⟩ \| φ\} y \land y \{⟨y, z⟩ \| ψ\} z) \leftrightarrow (φ \land ψ)$
40	39	exbii	$⊢ \exists y (x \{⟨x, y⟩ \| φ\} y \land y \{⟨y, z⟩ \| ψ\} z) \leftrightarrow \exists y (φ \land ψ)$
41	40	opabbii	$⊢ \{⟨x, z⟩ \| \exists y (x \{⟨x, y⟩ \| φ\} y \land y \{⟨y, z⟩ \| ψ\} z)\} = \{⟨x, z⟩ \| \exists y (φ \land ψ)\}$
42	1 36 41	3eqtri	$⊢ \{⟨y, z⟩ \| ψ\} \circ \{⟨x, y⟩ \| φ\} = \{⟨x, z⟩ \| \exists y (φ \land ψ)\}$

Metamath Proof Explorer

Theorem bj-opabco

Proof