Step | Hyp | Ref
| Expression |
1 | | opex 5379 |
. 2
⊢
〈𝐴, 𝐵〉 ∈ V |
2 | | brcap.3 |
. 2
⊢ 𝐶 ∈ V |
3 | | df-cap 34172 |
. 2
⊢ Cap =
(((V × V) × V) ∖ ran ((V ⊗ E ) △ (((◡1st ∘ E ) ∩ (◡2nd ∘ E )) ⊗
V))) |
4 | | brcap.1 |
. . . 4
⊢ 𝐴 ∈ V |
5 | | brcap.2 |
. . . 4
⊢ 𝐵 ∈ V |
6 | 4, 5 | opelvv 5628 |
. . 3
⊢
〈𝐴, 𝐵〉 ∈ (V ×
V) |
7 | | brxp 5636 |
. . 3
⊢
(〈𝐴, 𝐵〉((V × V) ×
V)𝐶 ↔ (〈𝐴, 𝐵〉 ∈ (V × V) ∧ 𝐶 ∈ V)) |
8 | 6, 2, 7 | mpbir2an 708 |
. 2
⊢
〈𝐴, 𝐵〉((V × V) ×
V)𝐶 |
9 | | epel 5498 |
. . . . . . 7
⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦) |
10 | | vex 3436 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
11 | 10, 1 | brcnv 5791 |
. . . . . . . 8
⊢ (𝑦◡1st 〈𝐴, 𝐵〉 ↔ 〈𝐴, 𝐵〉1st 𝑦) |
12 | 4, 5 | br1steq 33745 |
. . . . . . . 8
⊢
(〈𝐴, 𝐵〉1st 𝑦 ↔ 𝑦 = 𝐴) |
13 | 11, 12 | bitri 274 |
. . . . . . 7
⊢ (𝑦◡1st 〈𝐴, 𝐵〉 ↔ 𝑦 = 𝐴) |
14 | 9, 13 | anbi12ci 628 |
. . . . . 6
⊢ ((𝑥 E 𝑦 ∧ 𝑦◡1st 〈𝐴, 𝐵〉) ↔ (𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦)) |
15 | 14 | exbii 1850 |
. . . . 5
⊢
(∃𝑦(𝑥 E 𝑦 ∧ 𝑦◡1st 〈𝐴, 𝐵〉) ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦)) |
16 | | vex 3436 |
. . . . . 6
⊢ 𝑥 ∈ V |
17 | 16, 1 | brco 5779 |
. . . . 5
⊢ (𝑥(◡1st ∘ E )〈𝐴, 𝐵〉 ↔ ∃𝑦(𝑥 E 𝑦 ∧ 𝑦◡1st 〈𝐴, 𝐵〉)) |
18 | 4 | clel3 3592 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦)) |
19 | 15, 17, 18 | 3bitr4i 303 |
. . . 4
⊢ (𝑥(◡1st ∘ E )〈𝐴, 𝐵〉 ↔ 𝑥 ∈ 𝐴) |
20 | 10, 1 | brcnv 5791 |
. . . . . . . 8
⊢ (𝑦◡2nd 〈𝐴, 𝐵〉 ↔ 〈𝐴, 𝐵〉2nd 𝑦) |
21 | 4, 5 | br2ndeq 33746 |
. . . . . . . 8
⊢
(〈𝐴, 𝐵〉2nd 𝑦 ↔ 𝑦 = 𝐵) |
22 | 20, 21 | bitri 274 |
. . . . . . 7
⊢ (𝑦◡2nd 〈𝐴, 𝐵〉 ↔ 𝑦 = 𝐵) |
23 | 9, 22 | anbi12ci 628 |
. . . . . 6
⊢ ((𝑥 E 𝑦 ∧ 𝑦◡2nd 〈𝐴, 𝐵〉) ↔ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)) |
24 | 23 | exbii 1850 |
. . . . 5
⊢
(∃𝑦(𝑥 E 𝑦 ∧ 𝑦◡2nd 〈𝐴, 𝐵〉) ↔ ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)) |
25 | 16, 1 | brco 5779 |
. . . . 5
⊢ (𝑥(◡2nd ∘ E )〈𝐴, 𝐵〉 ↔ ∃𝑦(𝑥 E 𝑦 ∧ 𝑦◡2nd 〈𝐴, 𝐵〉)) |
26 | 5 | clel3 3592 |
. . . . 5
⊢ (𝑥 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)) |
27 | 24, 25, 26 | 3bitr4i 303 |
. . . 4
⊢ (𝑥(◡2nd ∘ E )〈𝐴, 𝐵〉 ↔ 𝑥 ∈ 𝐵) |
28 | 19, 27 | anbi12i 627 |
. . 3
⊢ ((𝑥(◡1st ∘ E )〈𝐴, 𝐵〉 ∧ 𝑥(◡2nd ∘ E )〈𝐴, 𝐵〉) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
29 | | brin 5126 |
. . 3
⊢ (𝑥((◡1st ∘ E ) ∩ (◡2nd ∘ E ))〈𝐴, 𝐵〉 ↔ (𝑥(◡1st ∘ E )〈𝐴, 𝐵〉 ∧ 𝑥(◡2nd ∘ E )〈𝐴, 𝐵〉)) |
30 | | elin 3903 |
. . 3
⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
31 | 28, 29, 30 | 3bitr4ri 304 |
. 2
⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ 𝑥((◡1st ∘ E ) ∩ (◡2nd ∘ E ))〈𝐴, 𝐵〉) |
32 | 1, 2, 3, 8, 31 | brtxpsd3 34198 |
1
⊢
(〈𝐴, 𝐵〉Cap𝐶 ↔ 𝐶 = (𝐴 ∩ 𝐵)) |