Theorem bj-opabco

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

	Ref	Expression
Assertion	bj-opabco	⊢ ( { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } ∘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) }

Proof

Step	Hyp	Ref	Expression
1		df-co	⊢ ( { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } ∘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑐 ∧ 𝑐 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑏 ) }
2		nfcv	⊢ Ⅎ 𝑥 𝑎
3		nfopab1	⊢ Ⅎ 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
4		nfcv	⊢ Ⅎ 𝑥 𝑐
5	2 3 4	nfbr	⊢ Ⅎ 𝑥 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑐
6		nfv	⊢ Ⅎ 𝑥 𝑐 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑏
7	5 6	nfan	⊢ Ⅎ 𝑥 ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑐 ∧ 𝑐 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑏 )
8	7	nfex	⊢ Ⅎ 𝑥 ∃ 𝑐 ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑐 ∧ 𝑐 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑏 )
9		nfv	⊢ Ⅎ 𝑧 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑐
10		nfcv	⊢ Ⅎ 𝑧 𝑐
11		nfopab2	⊢ Ⅎ 𝑧 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 }
12		nfcv	⊢ Ⅎ 𝑧 𝑏
13	10 11 12	nfbr	⊢ Ⅎ 𝑧 𝑐 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑏
14	9 13	nfan	⊢ Ⅎ 𝑧 ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑐 ∧ 𝑐 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑏 )
15	14	nfex	⊢ Ⅎ 𝑧 ∃ 𝑐 ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑐 ∧ 𝑐 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑏 )
16		nfv	⊢ Ⅎ 𝑎 ∃ 𝑦 ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 ∧ 𝑦 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑧 )
17		nfv	⊢ Ⅎ 𝑏 ∃ 𝑦 ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 ∧ 𝑦 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑧 )
18		nfv	⊢ Ⅎ 𝑦 ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑧 )
19		nfcv	⊢ Ⅎ 𝑦 𝑎
20		nfopab2	⊢ Ⅎ 𝑦 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
21		nfcv	⊢ Ⅎ 𝑦 𝑐
22	19 20 21	nfbr	⊢ Ⅎ 𝑦 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑐
23		nfopab1	⊢ Ⅎ 𝑦 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 }
24		nfcv	⊢ Ⅎ 𝑦 𝑏
25	21 23 24	nfbr	⊢ Ⅎ 𝑦 𝑐 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑏
26	22 25	nfan	⊢ Ⅎ 𝑦 ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑐 ∧ 𝑐 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑏 )
27	26	a1i	⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑧 ) → Ⅎ 𝑦 ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑐 ∧ 𝑐 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑏 ) )
28		simpll	⊢ ( ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑧 ) ∧ 𝑐 = 𝑦 ) → 𝑎 = 𝑥 )
29		simpr	⊢ ( ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑧 ) ∧ 𝑐 = 𝑦 ) → 𝑐 = 𝑦 )
30	28 29	breq12d	⊢ ( ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑧 ) ∧ 𝑐 = 𝑦 ) → ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑐 ↔ 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 ) )
31		simplr	⊢ ( ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑧 ) ∧ 𝑐 = 𝑦 ) → 𝑏 = 𝑧 )
32	29 31	breq12d	⊢ ( ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑧 ) ∧ 𝑐 = 𝑦 ) → ( 𝑐 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑏 ↔ 𝑦 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑧 ) )
33	30 32	anbi12d	⊢ ( ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑧 ) ∧ 𝑐 = 𝑦 ) → ( ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑐 ∧ 𝑐 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑏 ) ↔ ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 ∧ 𝑦 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑧 ) ) )
34	33	ex	⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑧 ) → ( 𝑐 = 𝑦 → ( ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑐 ∧ 𝑐 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑏 ) ↔ ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 ∧ 𝑦 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑧 ) ) ) )
35	18 27 34	cbvexdw	⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑧 ) → ( ∃ 𝑐 ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑐 ∧ 𝑐 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑏 ) ↔ ∃ 𝑦 ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 ∧ 𝑦 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑧 ) ) )
36	8 15 16 17 35	cbvopab	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ( 𝑎 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑐 ∧ 𝑐 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑏 ) } = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 ∧ 𝑦 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑧 ) }
37		bj-opelopabid	⊢ ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 ↔ 𝜑 )
38		bj-opelopabid	⊢ ( 𝑦 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑧 ↔ 𝜓 )
39	37 38	anbi12i	⊢ ( ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 ∧ 𝑦 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑧 ) ↔ ( 𝜑 ∧ 𝜓 ) )
40	39	exbii	⊢ ( ∃ 𝑦 ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 ∧ 𝑦 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑧 ) ↔ ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) )
41	40	opabbii	⊢ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 ∧ 𝑦 { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } 𝑧 ) } = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) }
42	1 36 41	3eqtri	⊢ ( { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } ∘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝜑 ∧ 𝜓 ) }