Metamath Proof Explorer


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 ( { ⟨ 𝑦 , 𝑧 ⟩ ∣ 𝜓 } ∘ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝜑𝜓 ) }