Step | Hyp | Ref
| Expression |
1 | | xpsnen.1 |
. . 3
⊢ 𝐴 ∈ V |
2 | | xpsnen.2 |
. . . 4
⊢ 𝐵 ∈ V |
3 | 2 | snex 4171 |
. . 3
⊢ {𝐵} ∈ V |
4 | 1, 3 | xpex 4726 |
. 2
⊢ (𝐴 × {𝐵}) ∈ V |
5 | | elxp 4628 |
. . 3
⊢ (𝑦 ∈ (𝐴 × {𝐵}) ↔ ∃𝑥∃𝑧(𝑦 = 〈𝑥, 𝑧〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ {𝐵}))) |
6 | | inteq 3834 |
. . . . . . . 8
⊢ (𝑦 = 〈𝑥, 𝑧〉 → ∩
𝑦 = ∩ 〈𝑥, 𝑧〉) |
7 | 6 | inteqd 3836 |
. . . . . . 7
⊢ (𝑦 = 〈𝑥, 𝑧〉 → ∩
∩ 𝑦 = ∩ ∩ 〈𝑥, 𝑧〉) |
8 | | vex 2733 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
9 | | vex 2733 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
10 | 8, 9 | op1stb 4463 |
. . . . . . 7
⊢ ∩ ∩ 〈𝑥, 𝑧〉 = 𝑥 |
11 | 7, 10 | eqtrdi 2219 |
. . . . . 6
⊢ (𝑦 = 〈𝑥, 𝑧〉 → ∩
∩ 𝑦 = 𝑥) |
12 | 11, 8 | eqeltrdi 2261 |
. . . . 5
⊢ (𝑦 = 〈𝑥, 𝑧〉 → ∩
∩ 𝑦 ∈ V) |
13 | 12 | adantr 274 |
. . . 4
⊢ ((𝑦 = 〈𝑥, 𝑧〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ {𝐵})) → ∩
∩ 𝑦 ∈ V) |
14 | 13 | exlimivv 1889 |
. . 3
⊢
(∃𝑥∃𝑧(𝑦 = 〈𝑥, 𝑧〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ {𝐵})) → ∩
∩ 𝑦 ∈ V) |
15 | 5, 14 | sylbi 120 |
. 2
⊢ (𝑦 ∈ (𝐴 × {𝐵}) → ∩ ∩ 𝑦
∈ V) |
16 | 8, 2 | opex 4214 |
. . 3
⊢
〈𝑥, 𝐵〉 ∈ V |
17 | 16 | a1i 9 |
. 2
⊢ (𝑥 ∈ 𝐴 → 〈𝑥, 𝐵〉 ∈ V) |
18 | | eqvisset 2740 |
. . . . 5
⊢ (𝑥 = ∩
∩ 𝑦 → ∩ ∩ 𝑦
∈ V) |
19 | | ancom 264 |
. . . . . . . . . . 11
⊢ (((𝑦 = 〈𝑥, 𝑧〉 ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ {𝐵}) ↔ (𝑧 ∈ {𝐵} ∧ (𝑦 = 〈𝑥, 𝑧〉 ∧ 𝑥 ∈ 𝐴))) |
20 | | anass 399 |
. . . . . . . . . . 11
⊢ (((𝑦 = 〈𝑥, 𝑧〉 ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ {𝐵}) ↔ (𝑦 = 〈𝑥, 𝑧〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ {𝐵}))) |
21 | | velsn 3600 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ {𝐵} ↔ 𝑧 = 𝐵) |
22 | 21 | anbi1i 455 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ {𝐵} ∧ (𝑦 = 〈𝑥, 𝑧〉 ∧ 𝑥 ∈ 𝐴)) ↔ (𝑧 = 𝐵 ∧ (𝑦 = 〈𝑥, 𝑧〉 ∧ 𝑥 ∈ 𝐴))) |
23 | 19, 20, 22 | 3bitr3i 209 |
. . . . . . . . . 10
⊢ ((𝑦 = 〈𝑥, 𝑧〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ {𝐵})) ↔ (𝑧 = 𝐵 ∧ (𝑦 = 〈𝑥, 𝑧〉 ∧ 𝑥 ∈ 𝐴))) |
24 | 23 | exbii 1598 |
. . . . . . . . 9
⊢
(∃𝑧(𝑦 = 〈𝑥, 𝑧〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ {𝐵})) ↔ ∃𝑧(𝑧 = 𝐵 ∧ (𝑦 = 〈𝑥, 𝑧〉 ∧ 𝑥 ∈ 𝐴))) |
25 | | opeq2 3766 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝐵 → 〈𝑥, 𝑧〉 = 〈𝑥, 𝐵〉) |
26 | 25 | eqeq2d 2182 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐵 → (𝑦 = 〈𝑥, 𝑧〉 ↔ 𝑦 = 〈𝑥, 𝐵〉)) |
27 | 26 | anbi1d 462 |
. . . . . . . . . 10
⊢ (𝑧 = 𝐵 → ((𝑦 = 〈𝑥, 𝑧〉 ∧ 𝑥 ∈ 𝐴) ↔ (𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴))) |
28 | 2, 27 | ceqsexv 2769 |
. . . . . . . . 9
⊢
(∃𝑧(𝑧 = 𝐵 ∧ (𝑦 = 〈𝑥, 𝑧〉 ∧ 𝑥 ∈ 𝐴)) ↔ (𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴)) |
29 | | inteq 3834 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 〈𝑥, 𝐵〉 → ∩
𝑦 = ∩ 〈𝑥, 𝐵〉) |
30 | 29 | inteqd 3836 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 〈𝑥, 𝐵〉 → ∩
∩ 𝑦 = ∩ ∩ 〈𝑥, 𝐵〉) |
31 | 8, 2 | op1stb 4463 |
. . . . . . . . . . . . 13
⊢ ∩ ∩ 〈𝑥, 𝐵〉 = 𝑥 |
32 | 30, 31 | eqtr2di 2220 |
. . . . . . . . . . . 12
⊢ (𝑦 = 〈𝑥, 𝐵〉 → 𝑥 = ∩ ∩ 𝑦) |
33 | 32 | pm4.71ri 390 |
. . . . . . . . . . 11
⊢ (𝑦 = 〈𝑥, 𝐵〉 ↔ (𝑥 = ∩ ∩ 𝑦
∧ 𝑦 = 〈𝑥, 𝐵〉)) |
34 | 33 | anbi1i 455 |
. . . . . . . . . 10
⊢ ((𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴) ↔ ((𝑥 = ∩ ∩ 𝑦
∧ 𝑦 = 〈𝑥, 𝐵〉) ∧ 𝑥 ∈ 𝐴)) |
35 | | anass 399 |
. . . . . . . . . 10
⊢ (((𝑥 = ∩
∩ 𝑦 ∧ 𝑦 = 〈𝑥, 𝐵〉) ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = ∩ ∩ 𝑦
∧ (𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴))) |
36 | 34, 35 | bitri 183 |
. . . . . . . . 9
⊢ ((𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 = ∩ ∩ 𝑦
∧ (𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴))) |
37 | 24, 28, 36 | 3bitri 205 |
. . . . . . . 8
⊢
(∃𝑧(𝑦 = 〈𝑥, 𝑧〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ {𝐵})) ↔ (𝑥 = ∩ ∩ 𝑦
∧ (𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴))) |
38 | 37 | exbii 1598 |
. . . . . . 7
⊢
(∃𝑥∃𝑧(𝑦 = 〈𝑥, 𝑧〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ {𝐵})) ↔ ∃𝑥(𝑥 = ∩ ∩ 𝑦
∧ (𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴))) |
39 | 5, 38 | bitri 183 |
. . . . . 6
⊢ (𝑦 ∈ (𝐴 × {𝐵}) ↔ ∃𝑥(𝑥 = ∩ ∩ 𝑦
∧ (𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴))) |
40 | | opeq1 3765 |
. . . . . . . . 9
⊢ (𝑥 = ∩
∩ 𝑦 → 〈𝑥, 𝐵〉 = 〈∩
∩ 𝑦, 𝐵〉) |
41 | 40 | eqeq2d 2182 |
. . . . . . . 8
⊢ (𝑥 = ∩
∩ 𝑦 → (𝑦 = 〈𝑥, 𝐵〉 ↔ 𝑦 = 〈∩ ∩ 𝑦,
𝐵〉)) |
42 | | eleq1 2233 |
. . . . . . . 8
⊢ (𝑥 = ∩
∩ 𝑦 → (𝑥 ∈ 𝐴 ↔ ∩ ∩ 𝑦
∈ 𝐴)) |
43 | 41, 42 | anbi12d 470 |
. . . . . . 7
⊢ (𝑥 = ∩
∩ 𝑦 → ((𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴) ↔ (𝑦 = 〈∩ ∩ 𝑦,
𝐵〉 ∧ ∩ ∩ 𝑦 ∈ 𝐴))) |
44 | 43 | ceqsexgv 2859 |
. . . . . 6
⊢ (∩ ∩ 𝑦 ∈ V → (∃𝑥(𝑥 = ∩ ∩ 𝑦
∧ (𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴)) ↔ (𝑦 = 〈∩ ∩ 𝑦,
𝐵〉 ∧ ∩ ∩ 𝑦 ∈ 𝐴))) |
45 | 39, 44 | syl5bb 191 |
. . . . 5
⊢ (∩ ∩ 𝑦 ∈ V → (𝑦 ∈ (𝐴 × {𝐵}) ↔ (𝑦 = 〈∩ ∩ 𝑦,
𝐵〉 ∧ ∩ ∩ 𝑦 ∈ 𝐴))) |
46 | 18, 45 | syl 14 |
. . . 4
⊢ (𝑥 = ∩
∩ 𝑦 → (𝑦 ∈ (𝐴 × {𝐵}) ↔ (𝑦 = 〈∩ ∩ 𝑦,
𝐵〉 ∧ ∩ ∩ 𝑦 ∈ 𝐴))) |
47 | 46 | pm5.32ri 452 |
. . 3
⊢ ((𝑦 ∈ (𝐴 × {𝐵}) ∧ 𝑥 = ∩ ∩ 𝑦)
↔ ((𝑦 = 〈∩ ∩ 𝑦, 𝐵〉 ∧ ∩
∩ 𝑦 ∈ 𝐴) ∧ 𝑥 = ∩ ∩ 𝑦)) |
48 | 32 | adantr 274 |
. . . . 5
⊢ ((𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴) → 𝑥 = ∩ ∩ 𝑦) |
49 | 48 | pm4.71i 389 |
. . . 4
⊢ ((𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴) ↔ ((𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = ∩ ∩ 𝑦)) |
50 | 43 | pm5.32ri 452 |
. . . 4
⊢ (((𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴) ∧ 𝑥 = ∩ ∩ 𝑦)
↔ ((𝑦 = 〈∩ ∩ 𝑦, 𝐵〉 ∧ ∩
∩ 𝑦 ∈ 𝐴) ∧ 𝑥 = ∩ ∩ 𝑦)) |
51 | 49, 50 | bitr2i 184 |
. . 3
⊢ (((𝑦 = 〈∩ ∩ 𝑦, 𝐵〉 ∧ ∩
∩ 𝑦 ∈ 𝐴) ∧ 𝑥 = ∩ ∩ 𝑦)
↔ (𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴)) |
52 | | ancom 264 |
. . 3
⊢ ((𝑦 = 〈𝑥, 𝐵〉 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 〈𝑥, 𝐵〉)) |
53 | 47, 51, 52 | 3bitri 205 |
. 2
⊢ ((𝑦 ∈ (𝐴 × {𝐵}) ∧ 𝑥 = ∩ ∩ 𝑦)
↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 〈𝑥, 𝐵〉)) |
54 | 4, 1, 15, 17, 53 | en2i 6748 |
1
⊢ (𝐴 × {𝐵}) ≈ 𝐴 |