Step | Hyp | Ref
| Expression |
1 | | xpsnen.1 |
. . 3
⊢ 𝐴 ∈ V |
2 | | snex 5356 |
. . 3
⊢ {𝐵} ∈ V |
3 | 1, 2 | xpex 7603 |
. 2
⊢ (𝐴 × {𝐵}) ∈ V |
4 | | elxp 5614 |
. . 3
⊢ (𝑦 ∈ (𝐴 × {𝐵}) ↔ ∃𝑥∃𝑧(𝑦 = 〈𝑥, 𝑧〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ {𝐵}))) |
5 | | inteq 4884 |
. . . . . . . 8
⊢ (𝑦 = 〈𝑥, 𝑧〉 → ∩
𝑦 = ∩ 〈𝑥, 𝑧〉) |
6 | 5 | inteqd 4886 |
. . . . . . 7
⊢ (𝑦 = 〈𝑥, 𝑧〉 → ∩
∩ 𝑦 = ∩ ∩ 〈𝑥, 𝑧〉) |
7 | | vex 3435 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
8 | | vex 3435 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
9 | 7, 8 | op1stb 5388 |
. . . . . . 7
⊢ ∩ ∩ 〈𝑥, 𝑧〉 = 𝑥 |
10 | 6, 9 | eqtrdi 2794 |
. . . . . 6
⊢ (𝑦 = 〈𝑥, 𝑧〉 → ∩
∩ 𝑦 = 𝑥) |
11 | 10, 7 | eqeltrdi 2847 |
. . . . 5
⊢ (𝑦 = 〈𝑥, 𝑧〉 → ∩
∩ 𝑦 ∈ V) |
12 | 11 | adantr 481 |
. . . 4
⊢ ((𝑦 = 〈𝑥, 𝑧〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ {𝐵})) → ∩
∩ 𝑦 ∈ V) |
13 | 12 | exlimivv 1935 |
. . 3
⊢
(∃𝑥∃𝑧(𝑦 = 〈𝑥, 𝑧〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ {𝐵})) → ∩
∩ 𝑦 ∈ V) |
14 | 4, 13 | sylbi 216 |
. 2
⊢ (𝑦 ∈ (𝐴 × {𝐵}) → ∩ ∩ 𝑦
∈ V) |
15 | | opex 5381 |
. . 3
⊢
〈𝑥, 𝐵〉 ∈ V |
16 | 15 | a1i 11 |
. 2
⊢ (𝑥 ∈ 𝐴 → 〈𝑥, 𝐵〉 ∈ V) |
17 | | eqvisset 3448 |
. . . . 5
⊢ (𝑥 = ∩
∩ 𝑦 → ∩ ∩ 𝑦
∈ V) |
18 | | ancom 461 |
. . . . . . . . . . 11
⊢ (((𝑦 = 〈𝑥, 𝑧〉 ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ {𝐵}) ↔ (𝑧 ∈ {𝐵} ∧ (𝑦 = 〈𝑥, 𝑧〉 ∧ 𝑥 ∈ 𝐴))) |
19 | | anass 469 |
. . . . . . . . . . 11
⊢ (((𝑦 = 〈𝑥, 𝑧〉 ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ {𝐵}) ↔ (𝑦 = 〈𝑥, 𝑧〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ {𝐵}))) |
20 | | velsn 4579 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ {𝐵} ↔ 𝑧 = 𝐵) |
21 | 20 | anbi1i 624 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ {𝐵} ∧ (𝑦 = 〈𝑥, 𝑧〉 ∧ 𝑥 ∈ 𝐴)) ↔ (𝑧 = 𝐵 ∧ (𝑦 = 〈𝑥, 𝑧〉 ∧ 𝑥 ∈ 𝐴))) |
22 | 18, 19, 21 | 3bitr3i 301 |
. . . . . . . . . 10
⊢ ((𝑦 = 〈𝑥, 𝑧〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ {𝐵})) ↔ (𝑧 = 𝐵 ∧ (𝑦 = 〈𝑥, 𝑧〉 ∧ 𝑥 ∈ 𝐴))) |
23 | 22 | exbii 1850 |
. . . . . . . . 9
⊢
(∃𝑧(𝑦 = 〈𝑥, 𝑧〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ {𝐵})) ↔ ∃𝑧(𝑧 = 𝐵 ∧ (𝑦 = 〈𝑥, 𝑧〉 ∧ 𝑥 ∈ 𝐴))) |
24 | | xpsnen.2 |
. . . . . . . . . 10
⊢ 𝐵 ∈ V |
25 | | opeq2 4807 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝐵 → 〈𝑥, 𝑧〉 = 〈𝑥, 𝐵〉) |
26 | 25 | eqeq2d 2749 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐵 → (𝑦 = 〈𝑥, 𝑧〉 ↔ 𝑦 = 〈𝑥, 𝐵〉)) |
27 | 26 | anbi1d 630 |
. . . . . . . . . 10
⊢ (𝑧 = 𝐵 → ((𝑦 = 〈𝑥, 𝑧〉 ∧ 𝑥 ∈ 𝐴) ↔ (𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴))) |
28 | 24, 27 | ceqsexv 3478 |
. . . . . . . . 9
⊢
(∃𝑧(𝑧 = 𝐵 ∧ (𝑦 = 〈𝑥, 𝑧〉 ∧ 𝑥 ∈ 𝐴)) ↔ (𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴)) |
29 | | inteq 4884 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 〈𝑥, 𝐵〉 → ∩
𝑦 = ∩ 〈𝑥, 𝐵〉) |
30 | 29 | inteqd 4886 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 〈𝑥, 𝐵〉 → ∩
∩ 𝑦 = ∩ ∩ 〈𝑥, 𝐵〉) |
31 | 7, 24 | op1stb 5388 |
. . . . . . . . . . . . 13
⊢ ∩ ∩ 〈𝑥, 𝐵〉 = 𝑥 |
32 | 30, 31 | eqtr2di 2795 |
. . . . . . . . . . . 12
⊢ (𝑦 = 〈𝑥, 𝐵〉 → 𝑥 = ∩ ∩ 𝑦) |
33 | 32 | pm4.71ri 561 |
. . . . . . . . . . 11
⊢ (𝑦 = 〈𝑥, 𝐵〉 ↔ (𝑥 = ∩ ∩ 𝑦
∧ 𝑦 = 〈𝑥, 𝐵〉)) |
34 | 33 | anbi1i 624 |
. . . . . . . . . 10
⊢ ((𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴) ↔ ((𝑥 = ∩ ∩ 𝑦
∧ 𝑦 = 〈𝑥, 𝐵〉) ∧ 𝑥 ∈ 𝐴)) |
35 | | anass 469 |
. . . . . . . . . 10
⊢ (((𝑥 = ∩
∩ 𝑦 ∧ 𝑦 = 〈𝑥, 𝐵〉) ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = ∩ ∩ 𝑦
∧ (𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴))) |
36 | 34, 35 | bitri 274 |
. . . . . . . . 9
⊢ ((𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = ∩ ∩ 𝑦
∧ (𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴))) |
37 | 23, 28, 36 | 3bitri 297 |
. . . . . . . 8
⊢
(∃𝑧(𝑦 = 〈𝑥, 𝑧〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ {𝐵})) ↔ (𝑥 = ∩ ∩ 𝑦
∧ (𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴))) |
38 | 37 | exbii 1850 |
. . . . . . 7
⊢
(∃𝑥∃𝑧(𝑦 = 〈𝑥, 𝑧〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ {𝐵})) ↔ ∃𝑥(𝑥 = ∩ ∩ 𝑦
∧ (𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴))) |
39 | 4, 38 | bitri 274 |
. . . . . 6
⊢ (𝑦 ∈ (𝐴 × {𝐵}) ↔ ∃𝑥(𝑥 = ∩ ∩ 𝑦
∧ (𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴))) |
40 | | opeq1 4806 |
. . . . . . . . 9
⊢ (𝑥 = ∩
∩ 𝑦 → 〈𝑥, 𝐵〉 = 〈∩
∩ 𝑦, 𝐵〉) |
41 | 40 | eqeq2d 2749 |
. . . . . . . 8
⊢ (𝑥 = ∩
∩ 𝑦 → (𝑦 = 〈𝑥, 𝐵〉 ↔ 𝑦 = 〈∩ ∩ 𝑦,
𝐵〉)) |
42 | | eleq1 2826 |
. . . . . . . 8
⊢ (𝑥 = ∩
∩ 𝑦 → (𝑥 ∈ 𝐴 ↔ ∩ ∩ 𝑦
∈ 𝐴)) |
43 | 41, 42 | anbi12d 631 |
. . . . . . 7
⊢ (𝑥 = ∩
∩ 𝑦 → ((𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴) ↔ (𝑦 = 〈∩ ∩ 𝑦,
𝐵〉 ∧ ∩ ∩ 𝑦 ∈ 𝐴))) |
44 | 43 | ceqsexgv 3585 |
. . . . . 6
⊢ (∩ ∩ 𝑦 ∈ V → (∃𝑥(𝑥 = ∩ ∩ 𝑦
∧ (𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴)) ↔ (𝑦 = 〈∩ ∩ 𝑦,
𝐵〉 ∧ ∩ ∩ 𝑦 ∈ 𝐴))) |
45 | 39, 44 | bitrid 282 |
. . . . 5
⊢ (∩ ∩ 𝑦 ∈ V → (𝑦 ∈ (𝐴 × {𝐵}) ↔ (𝑦 = 〈∩ ∩ 𝑦,
𝐵〉 ∧ ∩ ∩ 𝑦 ∈ 𝐴))) |
46 | 17, 45 | syl 17 |
. . . 4
⊢ (𝑥 = ∩
∩ 𝑦 → (𝑦 ∈ (𝐴 × {𝐵}) ↔ (𝑦 = 〈∩ ∩ 𝑦,
𝐵〉 ∧ ∩ ∩ 𝑦 ∈ 𝐴))) |
47 | 46 | pm5.32ri 576 |
. . 3
⊢ ((𝑦 ∈ (𝐴 × {𝐵}) ∧ 𝑥 = ∩ ∩ 𝑦)
↔ ((𝑦 = 〈∩ ∩ 𝑦, 𝐵〉 ∧ ∩
∩ 𝑦 ∈ 𝐴) ∧ 𝑥 = ∩ ∩ 𝑦)) |
48 | 32 | adantr 481 |
. . . . 5
⊢ ((𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴) → 𝑥 = ∩ ∩ 𝑦) |
49 | 48 | pm4.71i 560 |
. . . 4
⊢ ((𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴) ↔ ((𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = ∩ ∩ 𝑦)) |
50 | 43 | pm5.32ri 576 |
. . . 4
⊢ (((𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = ∩ ∩ 𝑦)
↔ ((𝑦 = 〈∩ ∩ 𝑦, 𝐵〉 ∧ ∩
∩ 𝑦 ∈ 𝐴) ∧ 𝑥 = ∩ ∩ 𝑦)) |
51 | 49, 50 | bitr2i 275 |
. . 3
⊢ (((𝑦 = 〈∩ ∩ 𝑦, 𝐵〉 ∧ ∩
∩ 𝑦 ∈ 𝐴) ∧ 𝑥 = ∩ ∩ 𝑦)
↔ (𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴)) |
52 | | ancom 461 |
. . 3
⊢ ((𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 〈𝑥, 𝐵〉)) |
53 | 47, 51, 52 | 3bitri 297 |
. 2
⊢ ((𝑦 ∈ (𝐴 × {𝐵}) ∧ 𝑥 = ∩ ∩ 𝑦)
↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 〈𝑥, 𝐵〉)) |
54 | 3, 1, 14, 16, 53 | en2i 8776 |
1
⊢ (𝐴 × {𝐵}) ≈ 𝐴 |