Step | Hyp | Ref
| Expression |
1 | | df-co 5526 |
. 2
⊢
({〈𝑦, 𝑧〉 ∣ 𝜓} ∘ {〈𝑥, 𝑦〉 ∣ 𝜑}) = {〈𝑎, 𝑏〉 ∣ ∃𝑐(𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ∧ 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏)} |
2 | | nfcv 2917 |
. . . . . 6
⊢
Ⅎ𝑥𝑎 |
3 | | nfopab1 5094 |
. . . . . 6
⊢
Ⅎ𝑥{〈𝑥, 𝑦〉 ∣ 𝜑} |
4 | | nfcv 2917 |
. . . . . 6
⊢
Ⅎ𝑥𝑐 |
5 | 2, 3, 4 | nfbr 5072 |
. . . . 5
⊢
Ⅎ𝑥 𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 |
6 | | nfv 1916 |
. . . . 5
⊢
Ⅎ𝑥 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏 |
7 | 5, 6 | nfan 1901 |
. . . 4
⊢
Ⅎ𝑥(𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ∧ 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏) |
8 | 7 | nfex 2333 |
. . 3
⊢
Ⅎ𝑥∃𝑐(𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ∧ 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏) |
9 | | nfv 1916 |
. . . . 5
⊢
Ⅎ𝑧 𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 |
10 | | nfcv 2917 |
. . . . . 6
⊢
Ⅎ𝑧𝑐 |
11 | | nfopab2 5095 |
. . . . . 6
⊢
Ⅎ𝑧{〈𝑦, 𝑧〉 ∣ 𝜓} |
12 | | nfcv 2917 |
. . . . . 6
⊢
Ⅎ𝑧𝑏 |
13 | 10, 11, 12 | nfbr 5072 |
. . . . 5
⊢
Ⅎ𝑧 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏 |
14 | 9, 13 | nfan 1901 |
. . . 4
⊢
Ⅎ𝑧(𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ∧ 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏) |
15 | 14 | nfex 2333 |
. . 3
⊢
Ⅎ𝑧∃𝑐(𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ∧ 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏) |
16 | | nfv 1916 |
. . 3
⊢
Ⅎ𝑎∃𝑦(𝑥{〈𝑥, 𝑦〉 ∣ 𝜑}𝑦 ∧ 𝑦{〈𝑦, 𝑧〉 ∣ 𝜓}𝑧) |
17 | | nfv 1916 |
. . 3
⊢
Ⅎ𝑏∃𝑦(𝑥{〈𝑥, 𝑦〉 ∣ 𝜑}𝑦 ∧ 𝑦{〈𝑦, 𝑧〉 ∣ 𝜓}𝑧) |
18 | | nfv 1916 |
. . . 4
⊢
Ⅎ𝑦(𝑎 = 𝑥 ∧ 𝑏 = 𝑧) |
19 | | nfcv 2917 |
. . . . . . 7
⊢
Ⅎ𝑦𝑎 |
20 | | nfopab2 5095 |
. . . . . . 7
⊢
Ⅎ𝑦{〈𝑥, 𝑦〉 ∣ 𝜑} |
21 | | nfcv 2917 |
. . . . . . 7
⊢
Ⅎ𝑦𝑐 |
22 | 19, 20, 21 | nfbr 5072 |
. . . . . 6
⊢
Ⅎ𝑦 𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 |
23 | | nfopab1 5094 |
. . . . . . 7
⊢
Ⅎ𝑦{〈𝑦, 𝑧〉 ∣ 𝜓} |
24 | | nfcv 2917 |
. . . . . . 7
⊢
Ⅎ𝑦𝑏 |
25 | 21, 23, 24 | nfbr 5072 |
. . . . . 6
⊢
Ⅎ𝑦 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏 |
26 | 22, 25 | nfan 1901 |
. . . . 5
⊢
Ⅎ𝑦(𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ∧ 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏) |
27 | 26 | a1i 11 |
. . . 4
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑧) → Ⅎ𝑦(𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ∧ 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏)) |
28 | | simpll 767 |
. . . . . . 7
⊢ (((𝑎 = 𝑥 ∧ 𝑏 = 𝑧) ∧ 𝑐 = 𝑦) → 𝑎 = 𝑥) |
29 | | simpr 489 |
. . . . . . 7
⊢ (((𝑎 = 𝑥 ∧ 𝑏 = 𝑧) ∧ 𝑐 = 𝑦) → 𝑐 = 𝑦) |
30 | 28, 29 | breq12d 5038 |
. . . . . 6
⊢ (((𝑎 = 𝑥 ∧ 𝑏 = 𝑧) ∧ 𝑐 = 𝑦) → (𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ↔ 𝑥{〈𝑥, 𝑦〉 ∣ 𝜑}𝑦)) |
31 | | simplr 769 |
. . . . . . 7
⊢ (((𝑎 = 𝑥 ∧ 𝑏 = 𝑧) ∧ 𝑐 = 𝑦) → 𝑏 = 𝑧) |
32 | 29, 31 | breq12d 5038 |
. . . . . 6
⊢ (((𝑎 = 𝑥 ∧ 𝑏 = 𝑧) ∧ 𝑐 = 𝑦) → (𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏 ↔ 𝑦{〈𝑦, 𝑧〉 ∣ 𝜓}𝑧)) |
33 | 30, 32 | anbi12d 634 |
. . . . 5
⊢ (((𝑎 = 𝑥 ∧ 𝑏 = 𝑧) ∧ 𝑐 = 𝑦) → ((𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ∧ 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏) ↔ (𝑥{〈𝑥, 𝑦〉 ∣ 𝜑}𝑦 ∧ 𝑦{〈𝑦, 𝑧〉 ∣ 𝜓}𝑧))) |
34 | 33 | ex 417 |
. . . 4
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑧) → (𝑐 = 𝑦 → ((𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ∧ 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏) ↔ (𝑥{〈𝑥, 𝑦〉 ∣ 𝜑}𝑦 ∧ 𝑦{〈𝑦, 𝑧〉 ∣ 𝜓}𝑧)))) |
35 | 18, 27, 34 | cbvexdw 2349 |
. . 3
⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑧) → (∃𝑐(𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ∧ 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏) ↔ ∃𝑦(𝑥{〈𝑥, 𝑦〉 ∣ 𝜑}𝑦 ∧ 𝑦{〈𝑦, 𝑧〉 ∣ 𝜓}𝑧))) |
36 | 8, 15, 16, 17, 35 | cbvopab 5096 |
. 2
⊢
{〈𝑎, 𝑏〉 ∣ ∃𝑐(𝑎{〈𝑥, 𝑦〉 ∣ 𝜑}𝑐 ∧ 𝑐{〈𝑦, 𝑧〉 ∣ 𝜓}𝑏)} = {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥{〈𝑥, 𝑦〉 ∣ 𝜑}𝑦 ∧ 𝑦{〈𝑦, 𝑧〉 ∣ 𝜓}𝑧)} |
37 | | bj-opelopabid 34867 |
. . . . 5
⊢ (𝑥{〈𝑥, 𝑦〉 ∣ 𝜑}𝑦 ↔ 𝜑) |
38 | | bj-opelopabid 34867 |
. . . . 5
⊢ (𝑦{〈𝑦, 𝑧〉 ∣ 𝜓}𝑧 ↔ 𝜓) |
39 | 37, 38 | anbi12i 630 |
. . . 4
⊢ ((𝑥{〈𝑥, 𝑦〉 ∣ 𝜑}𝑦 ∧ 𝑦{〈𝑦, 𝑧〉 ∣ 𝜓}𝑧) ↔ (𝜑 ∧ 𝜓)) |
40 | 39 | exbii 1850 |
. . 3
⊢
(∃𝑦(𝑥{〈𝑥, 𝑦〉 ∣ 𝜑}𝑦 ∧ 𝑦{〈𝑦, 𝑧〉 ∣ 𝜓}𝑧) ↔ ∃𝑦(𝜑 ∧ 𝜓)) |
41 | 40 | opabbii 5092 |
. 2
⊢
{〈𝑥, 𝑧〉 ∣ ∃𝑦(𝑥{〈𝑥, 𝑦〉 ∣ 𝜑}𝑦 ∧ 𝑦{〈𝑦, 𝑧〉 ∣ 𝜓}𝑧)} = {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝜑 ∧ 𝜓)} |
42 | 1, 36, 41 | 3eqtri 2786 |
1
⊢
({〈𝑦, 𝑧〉 ∣ 𝜓} ∘ {〈𝑥, 𝑦〉 ∣ 𝜑}) = {〈𝑥, 𝑧〉 ∣ ∃𝑦(𝜑 ∧ 𝜓)} |