Proof of Theorem relintab
Step | Hyp | Ref
| Expression |
1 | | cnvcnv 5586 |
. . 3
⊢ ◡◡∩ {𝑥 ∣ 𝜑} = (∩ {𝑥 ∣ 𝜑} ∩ (V × V)) |
2 | | incom 3805 |
. . 3
⊢ (∩ {𝑥
∣ 𝜑} ∩ (V ×
V)) = ((V × V) ∩ ∩ {𝑥 ∣ 𝜑}) |
3 | 1, 2 | eqtri 2644 |
. 2
⊢ ◡◡∩ {𝑥 ∣ 𝜑} = ((V × V) ∩ ∩ {𝑥
∣ 𝜑}) |
4 | | dfrel2 5583 |
. . 3
⊢ (Rel
∩ {𝑥 ∣ 𝜑} ↔ ◡◡∩ {𝑥 ∣ 𝜑} = ∩ {𝑥 ∣ 𝜑}) |
5 | 4 | biimpi 206 |
. 2
⊢ (Rel
∩ {𝑥 ∣ 𝜑} → ◡◡∩ {𝑥 ∣ 𝜑} = ∩ {𝑥 ∣ 𝜑}) |
6 | | relintabex 37887 |
. . . 4
⊢ (Rel
∩ {𝑥 ∣ 𝜑} → ∃𝑥𝜑) |
7 | 6 | xpinintabd 37886 |
. . 3
⊢ (Rel
∩ {𝑥 ∣ 𝜑} → ((V × V) ∩ ∩ {𝑥
∣ 𝜑}) = ∩ {𝑤
∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ((V × V) ∩ 𝑥) ∧ 𝜑)}) |
8 | | incom 3805 |
. . . . . . . . . 10
⊢ ((V
× V) ∩ 𝑥) =
(𝑥 ∩ (V ×
V)) |
9 | | cnvcnv 5586 |
. . . . . . . . . 10
⊢ ◡◡𝑥 = (𝑥 ∩ (V × V)) |
10 | 8, 9 | eqtr4i 2647 |
. . . . . . . . 9
⊢ ((V
× V) ∩ 𝑥) = ◡◡𝑥 |
11 | 10 | eqeq2i 2634 |
. . . . . . . 8
⊢ (𝑤 = ((V × V) ∩ 𝑥) ↔ 𝑤 = ◡◡𝑥) |
12 | 11 | anbi1i 731 |
. . . . . . 7
⊢ ((𝑤 = ((V × V) ∩ 𝑥) ∧ 𝜑) ↔ (𝑤 = ◡◡𝑥 ∧ 𝜑)) |
13 | 12 | exbii 1774 |
. . . . . 6
⊢
(∃𝑥(𝑤 = ((V × V) ∩ 𝑥) ∧ 𝜑) ↔ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜑)) |
14 | 13 | a1i 11 |
. . . . 5
⊢ (𝑤 ∈ 𝒫 (V × V)
→ (∃𝑥(𝑤 = ((V × V) ∩ 𝑥) ∧ 𝜑) ↔ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜑))) |
15 | 14 | rabbiia 3185 |
. . . 4
⊢ {𝑤 ∈ 𝒫 (V × V)
∣ ∃𝑥(𝑤 = ((V × V) ∩ 𝑥) ∧ 𝜑)} = {𝑤 ∈ 𝒫 (V × V) ∣
∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜑)} |
16 | 15 | inteqi 4479 |
. . 3
⊢ ∩ {𝑤
∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ((V × V) ∩ 𝑥) ∧ 𝜑)} = ∩ {𝑤 ∈ 𝒫 (V × V)
∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜑)} |
17 | 7, 16 | syl6eq 2672 |
. 2
⊢ (Rel
∩ {𝑥 ∣ 𝜑} → ((V × V) ∩ ∩ {𝑥
∣ 𝜑}) = ∩ {𝑤
∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜑)}) |
18 | 3, 5, 17 | 3eqtr3a 2680 |
1
⊢ (Rel
∩ {𝑥 ∣ 𝜑} → ∩ {𝑥 ∣ 𝜑} = ∩ {𝑤 ∈ 𝒫 (V × V)
∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜑)}) |