Proof of Theorem relintab
Step | Hyp | Ref
| Expression |
1 | | cnvcnv 5505 |
. . 3
⊢ ◡◡∩ {𝑥 ∣ 𝜑} = (∩ {𝑥 ∣ 𝜑} ∩ (V × V)) |
2 | | incom 3767 |
. . 3
⊢ (∩ {𝑥
∣ 𝜑} ∩ (V ×
V)) = ((V × V) ∩ ∩ {𝑥 ∣ 𝜑}) |
3 | 1, 2 | eqtri 2632 |
. 2
⊢ ◡◡∩ {𝑥 ∣ 𝜑} = ((V × V) ∩ ∩ {𝑥
∣ 𝜑}) |
4 | | dfrel2 5502 |
. . 3
⊢ (Rel
∩ {𝑥 ∣ 𝜑} ↔ ◡◡∩ {𝑥 ∣ 𝜑} = ∩ {𝑥 ∣ 𝜑}) |
5 | 4 | biimpi 205 |
. 2
⊢ (Rel
∩ {𝑥 ∣ 𝜑} → ◡◡∩ {𝑥 ∣ 𝜑} = ∩ {𝑥 ∣ 𝜑}) |
6 | | relintabex 36906 |
. . . 4
⊢ (Rel
∩ {𝑥 ∣ 𝜑} → ∃𝑥𝜑) |
7 | 6 | xpinintabd 36905 |
. . 3
⊢ (Rel
∩ {𝑥 ∣ 𝜑} → ((V × V) ∩ ∩ {𝑥
∣ 𝜑}) = ∩ {𝑤
∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ((V × V) ∩ 𝑥) ∧ 𝜑)}) |
8 | | incom 3767 |
. . . . . . . . . 10
⊢ ((V
× V) ∩ 𝑥) =
(𝑥 ∩ (V ×
V)) |
9 | | cnvcnv 5505 |
. . . . . . . . . 10
⊢ ◡◡𝑥 = (𝑥 ∩ (V × V)) |
10 | 8, 9 | eqtr4i 2635 |
. . . . . . . . 9
⊢ ((V
× V) ∩ 𝑥) = ◡◡𝑥 |
11 | 10 | eqeq2i 2622 |
. . . . . . . 8
⊢ (𝑤 = ((V × V) ∩ 𝑥) ↔ 𝑤 = ◡◡𝑥) |
12 | 11 | anbi1i 727 |
. . . . . . 7
⊢ ((𝑤 = ((V × V) ∩ 𝑥) ∧ 𝜑) ↔ (𝑤 = ◡◡𝑥 ∧ 𝜑)) |
13 | 12 | exbii 1764 |
. . . . . 6
⊢
(∃𝑥(𝑤 = ((V × V) ∩ 𝑥) ∧ 𝜑) ↔ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜑)) |
14 | 13 | a1i 11 |
. . . . 5
⊢ (𝑤 ∈ 𝒫 (V × V)
→ (∃𝑥(𝑤 = ((V × V) ∩ 𝑥) ∧ 𝜑) ↔ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜑))) |
15 | 14 | rabbiia 3161 |
. . . 4
⊢ {𝑤 ∈ 𝒫 (V × V)
∣ ∃𝑥(𝑤 = ((V × V) ∩ 𝑥) ∧ 𝜑)} = {𝑤 ∈ 𝒫 (V × V) ∣
∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜑)} |
16 | 15 | inteqi 4414 |
. . 3
⊢ ∩ {𝑤
∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ((V × V) ∩ 𝑥) ∧ 𝜑)} = ∩ {𝑤 ∈ 𝒫 (V × V)
∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜑)} |
17 | 7, 16 | syl6eq 2660 |
. 2
⊢ (Rel
∩ {𝑥 ∣ 𝜑} → ((V × V) ∩ ∩ {𝑥
∣ 𝜑}) = ∩ {𝑤
∈ 𝒫 (V × V) ∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜑)}) |
18 | 3, 5, 17 | 3eqtr3a 2668 |
1
⊢ (Rel
∩ {𝑥 ∣ 𝜑} → ∩ {𝑥 ∣ 𝜑} = ∩ {𝑤 ∈ 𝒫 (V × V)
∣ ∃𝑥(𝑤 = ◡◡𝑥 ∧ 𝜑)}) |