Proof of Theorem copsex2b
Step | Hyp | Ref
| Expression |
1 | | eqcom 2745 |
. . . . . . 7
⊢
(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ↔ 〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉) |
2 | | vex 3426 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
3 | | vex 3426 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
4 | 2, 3 | opth 5385 |
. . . . . . 7
⊢
(〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉 ↔ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) |
5 | 1, 4 | bitri 274 |
. . . . . 6
⊢
(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ↔ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) |
6 | | eqvisset 3439 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → 𝐴 ∈ V) |
7 | | eqvisset 3439 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → 𝐵 ∈ V) |
8 | 6, 7 | anim12i 612 |
. . . . . 6
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
9 | 5, 8 | sylbi 216 |
. . . . 5
⊢
(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
10 | 9 | adantr 480 |
. . . 4
⊢
((〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
11 | 10 | exlimivv 1936 |
. . 3
⊢
(∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
12 | 11 | anim2i 616 |
. 2
⊢ ((𝜑 ∧ ∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓)) → (𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V))) |
13 | | simpl 482 |
. . 3
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
14 | 13 | anim2i 616 |
. 2
⊢ ((𝜑 ∧ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒)) → (𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V))) |
15 | | copsex2b.xph |
. . . . 5
⊢ (𝜑 → ∀𝑥𝜑) |
16 | | ax-5 1914 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ∀𝑥(𝐴 ∈ V ∧ 𝐵 ∈ V)) |
17 | 15, 16 | hban 2300 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → ∀𝑥(𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V))) |
18 | | copsex2b.yph |
. . . . 5
⊢ (𝜑 → ∀𝑦𝜑) |
19 | | ax-5 1914 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ∀𝑦(𝐴 ∈ V ∧ 𝐵 ∈ V)) |
20 | 18, 19 | hban 2300 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → ∀𝑦(𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V))) |
21 | | copsex2b.xch |
. . . . 5
⊢ (𝜑 → Ⅎ𝑥𝜒) |
22 | 21 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → Ⅎ𝑥𝜒) |
23 | | copsex2b.ych |
. . . . 5
⊢ (𝜑 → Ⅎ𝑦𝜒) |
24 | 23 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → Ⅎ𝑦𝜒) |
25 | | simprl 767 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → 𝐴 ∈ V) |
26 | | simprr 769 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → 𝐵 ∈ V) |
27 | | copsex2b.is |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) |
28 | 27 | adantlr 711 |
. . . 4
⊢ (((𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) |
29 | 17, 20, 22, 24, 25, 26, 28 | copsex2d 35237 |
. . 3
⊢ ((𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ 𝜒)) |
30 | | ibar 528 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝜒 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒))) |
31 | 30 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → (𝜒 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒))) |
32 | 29, 31 | bitrd 278 |
. 2
⊢ ((𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒))) |
33 | 12, 14, 32 | pm5.21nd 798 |
1
⊢ (𝜑 → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒))) |