| Step | Hyp | Ref
| Expression |
| 1 | | opex 5469 |
. 2
⊢
〈𝐴, 𝐵〉 ∈ V |
| 2 | | brcap.3 |
. 2
⊢ 𝐶 ∈ V |
| 3 | | df-cap 35871 |
. 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 5725 |
. . 3
⊢
〈𝐴, 𝐵〉 ∈ (V ×
V) |
| 7 | | brxp 5734 |
. . 3
⊢
(〈𝐴, 𝐵〉((V × V) ×
V)𝐶 ↔ (〈𝐴, 𝐵〉 ∈ (V × V) ∧ 𝐶 ∈ V)) |
| 8 | 6, 2, 7 | mpbir2an 711 |
. 2
⊢
〈𝐴, 𝐵〉((V × V) ×
V)𝐶 |
| 9 | | epel 5587 |
. . . . . . 7
⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦) |
| 10 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
| 11 | 10, 1 | brcnv 5893 |
. . . . . . . 8
⊢ (𝑦◡1st 〈𝐴, 𝐵〉 ↔ 〈𝐴, 𝐵〉1st 𝑦) |
| 12 | 4, 5 | br1steq 35771 |
. . . . . . . 8
⊢
(〈𝐴, 𝐵〉1st 𝑦 ↔ 𝑦 = 𝐴) |
| 13 | 11, 12 | bitri 275 |
. . . . . . 7
⊢ (𝑦◡1st 〈𝐴, 𝐵〉 ↔ 𝑦 = 𝐴) |
| 14 | 9, 13 | anbi12ci 629 |
. . . . . 6
⊢ ((𝑥 E 𝑦 ∧ 𝑦◡1st 〈𝐴, 𝐵〉) ↔ (𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦)) |
| 15 | 14 | exbii 1848 |
. . . . 5
⊢
(∃𝑦(𝑥 E 𝑦 ∧ 𝑦◡1st 〈𝐴, 𝐵〉) ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦)) |
| 16 | | vex 3484 |
. . . . . 6
⊢ 𝑥 ∈ V |
| 17 | 16, 1 | brco 5881 |
. . . . 5
⊢ (𝑥(◡1st ∘ E )〈𝐴, 𝐵〉 ↔ ∃𝑦(𝑥 E 𝑦 ∧ 𝑦◡1st 〈𝐴, 𝐵〉)) |
| 18 | 4 | clel3 3662 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦)) |
| 19 | 15, 17, 18 | 3bitr4i 303 |
. . . 4
⊢ (𝑥(◡1st ∘ E )〈𝐴, 𝐵〉 ↔ 𝑥 ∈ 𝐴) |
| 20 | 10, 1 | brcnv 5893 |
. . . . . . . 8
⊢ (𝑦◡2nd 〈𝐴, 𝐵〉 ↔ 〈𝐴, 𝐵〉2nd 𝑦) |
| 21 | 4, 5 | br2ndeq 35772 |
. . . . . . . 8
⊢
(〈𝐴, 𝐵〉2nd 𝑦 ↔ 𝑦 = 𝐵) |
| 22 | 20, 21 | bitri 275 |
. . . . . . 7
⊢ (𝑦◡2nd 〈𝐴, 𝐵〉 ↔ 𝑦 = 𝐵) |
| 23 | 9, 22 | anbi12ci 629 |
. . . . . 6
⊢ ((𝑥 E 𝑦 ∧ 𝑦◡2nd 〈𝐴, 𝐵〉) ↔ (𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)) |
| 24 | 23 | exbii 1848 |
. . . . 5
⊢
(∃𝑦(𝑥 E 𝑦 ∧ 𝑦◡2nd 〈𝐴, 𝐵〉) ↔ ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)) |
| 25 | 16, 1 | brco 5881 |
. . . . 5
⊢ (𝑥(◡2nd ∘ E )〈𝐴, 𝐵〉 ↔ ∃𝑦(𝑥 E 𝑦 ∧ 𝑦◡2nd 〈𝐴, 𝐵〉)) |
| 26 | 5 | clel3 3662 |
. . . . 5
⊢ (𝑥 ∈ 𝐵 ↔ ∃𝑦(𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦)) |
| 27 | 24, 25, 26 | 3bitr4i 303 |
. . . 4
⊢ (𝑥(◡2nd ∘ E )〈𝐴, 𝐵〉 ↔ 𝑥 ∈ 𝐵) |
| 28 | 19, 27 | anbi12i 628 |
. . 3
⊢ ((𝑥(◡1st ∘ E )〈𝐴, 𝐵〉 ∧ 𝑥(◡2nd ∘ E )〈𝐴, 𝐵〉) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
| 29 | | brin 5195 |
. . 3
⊢ (𝑥((◡1st ∘ E ) ∩ (◡2nd ∘ E ))〈𝐴, 𝐵〉 ↔ (𝑥(◡1st ∘ E )〈𝐴, 𝐵〉 ∧ 𝑥(◡2nd ∘ E )〈𝐴, 𝐵〉)) |
| 30 | | elin 3967 |
. . 3
⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
| 31 | 28, 29, 30 | 3bitr4ri 304 |
. 2
⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ 𝑥((◡1st ∘ E ) ∩ (◡2nd ∘ E ))〈𝐴, 𝐵〉) |
| 32 | 1, 2, 3, 8, 31 | brtxpsd3 35897 |
1
⊢
(〈𝐴, 𝐵〉Cap𝐶 ↔ 𝐶 = (𝐴 ∩ 𝐵)) |