Proof of Theorem copsex2g
Step | Hyp | Ref
| Expression |
1 | | elisset 2744 |
. 2
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 = 𝐴) |
2 | | elisset 2744 |
. 2
⊢ (𝐵 ∈ 𝑊 → ∃𝑦 𝑦 = 𝐵) |
3 | | eeanv 1925 |
. . 3
⊢
(∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)) |
4 | | nfe1 1489 |
. . . . 5
⊢
Ⅎ𝑥∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
5 | | nfv 1521 |
. . . . 5
⊢
Ⅎ𝑥𝜓 |
6 | 4, 5 | nfbi 1582 |
. . . 4
⊢
Ⅎ𝑥(∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓) |
7 | | nfe1 1489 |
. . . . . . 7
⊢
Ⅎ𝑦∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
8 | 7 | nfex 1630 |
. . . . . 6
⊢
Ⅎ𝑦∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) |
9 | | nfv 1521 |
. . . . . 6
⊢
Ⅎ𝑦𝜓 |
10 | 8, 9 | nfbi 1582 |
. . . . 5
⊢
Ⅎ𝑦(∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓) |
11 | | opeq12 3767 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉) |
12 | | copsexg 4229 |
. . . . . . . 8
⊢
(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 → (𝜑 ↔ ∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
13 | 12 | eqcoms 2173 |
. . . . . . 7
⊢
(〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉 → (𝜑 ↔ ∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
14 | 11, 13 | syl 14 |
. . . . . 6
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ ∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑))) |
15 | | copsex2g.1 |
. . . . . 6
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) |
16 | 14, 15 | bitr3d 189 |
. . . . 5
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓)) |
17 | 10, 16 | exlimi 1587 |
. . . 4
⊢
(∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓)) |
18 | 6, 17 | exlimi 1587 |
. . 3
⊢
(∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓)) |
19 | 3, 18 | sylbir 134 |
. 2
⊢
((∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓)) |
20 | 1, 2, 19 | syl2an 287 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ 𝜓)) |