Proof of Theorem opreuopreu
| Step | Hyp | Ref
| Expression |
| 1 | | elxpi 5707 |
. . . 4
⊢ (𝑝 ∈ (𝐴 × 𝐵) → ∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵))) |
| 2 | | simprl 771 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵))) → 𝑝 = 〈𝑎, 𝑏〉) |
| 3 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑎 ∈ V |
| 4 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑏 ∈ V |
| 5 | 3, 4 | op1st 8022 |
. . . . . . . . . . . . . 14
⊢
(1st ‘〈𝑎, 𝑏〉) = 𝑎 |
| 6 | 5 | eqcomi 2746 |
. . . . . . . . . . . . 13
⊢ 𝑎 = (1st
‘〈𝑎, 𝑏〉) |
| 7 | 3, 4 | op2nd 8023 |
. . . . . . . . . . . . . 14
⊢
(2nd ‘〈𝑎, 𝑏〉) = 𝑏 |
| 8 | 7 | eqcomi 2746 |
. . . . . . . . . . . . 13
⊢ 𝑏 = (2nd
‘〈𝑎, 𝑏〉) |
| 9 | 6, 8 | pm3.2i 470 |
. . . . . . . . . . . 12
⊢ (𝑎 = (1st
‘〈𝑎, 𝑏〉) ∧ 𝑏 = (2nd ‘〈𝑎, 𝑏〉)) |
| 10 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 〈𝑎, 𝑏〉 → (1st ‘𝑝) = (1st
‘〈𝑎, 𝑏〉)) |
| 11 | 10 | eqeq2d 2748 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 〈𝑎, 𝑏〉 → (𝑎 = (1st ‘𝑝) ↔ 𝑎 = (1st ‘〈𝑎, 𝑏〉))) |
| 12 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 〈𝑎, 𝑏〉 → (2nd ‘𝑝) = (2nd
‘〈𝑎, 𝑏〉)) |
| 13 | 12 | eqeq2d 2748 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 〈𝑎, 𝑏〉 → (𝑏 = (2nd ‘𝑝) ↔ 𝑏 = (2nd ‘〈𝑎, 𝑏〉))) |
| 14 | 11, 13 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ (𝑝 = 〈𝑎, 𝑏〉 → ((𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝)) ↔ (𝑎 = (1st ‘〈𝑎, 𝑏〉) ∧ 𝑏 = (2nd ‘〈𝑎, 𝑏〉)))) |
| 15 | 9, 14 | mpbiri 258 |
. . . . . . . . . . 11
⊢ (𝑝 = 〈𝑎, 𝑏〉 → (𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝))) |
| 16 | | opreuopreu.a |
. . . . . . . . . . 11
⊢ ((𝑎 = (1st ‘𝑝) ∧ 𝑏 = (2nd ‘𝑝)) → (𝜓 ↔ 𝜑)) |
| 17 | 15, 16 | syl 17 |
. . . . . . . . . 10
⊢ (𝑝 = 〈𝑎, 𝑏〉 → (𝜓 ↔ 𝜑)) |
| 18 | 17 | biimprd 248 |
. . . . . . . . 9
⊢ (𝑝 = 〈𝑎, 𝑏〉 → (𝜑 → 𝜓)) |
| 19 | 18 | adantr 480 |
. . . . . . . 8
⊢ ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝜑 → 𝜓)) |
| 20 | 19 | impcom 407 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵))) → 𝜓) |
| 21 | 2, 20 | jca 511 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵))) → (𝑝 = 〈𝑎, 𝑏〉 ∧ 𝜓)) |
| 22 | 21 | ex 412 |
. . . . 5
⊢ (𝜑 → ((𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑝 = 〈𝑎, 𝑏〉 ∧ 𝜓))) |
| 23 | 22 | 2eximdv 1919 |
. . . 4
⊢ (𝜑 → (∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝜓))) |
| 24 | 1, 23 | syl5com 31 |
. . 3
⊢ (𝑝 ∈ (𝐴 × 𝐵) → (𝜑 → ∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝜓))) |
| 25 | 17 | biimpa 476 |
. . . . 5
⊢ ((𝑝 = 〈𝑎, 𝑏〉 ∧ 𝜓) → 𝜑) |
| 26 | 25 | a1i 11 |
. . . 4
⊢ (𝑝 ∈ (𝐴 × 𝐵) → ((𝑝 = 〈𝑎, 𝑏〉 ∧ 𝜓) → 𝜑)) |
| 27 | 26 | exlimdvv 1934 |
. . 3
⊢ (𝑝 ∈ (𝐴 × 𝐵) → (∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝜓) → 𝜑)) |
| 28 | 24, 27 | impbid 212 |
. 2
⊢ (𝑝 ∈ (𝐴 × 𝐵) → (𝜑 ↔ ∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝜓))) |
| 29 | 28 | reubiia 3387 |
1
⊢
(∃!𝑝 ∈
(𝐴 × 𝐵)𝜑 ↔ ∃!𝑝 ∈ (𝐴 × 𝐵)∃𝑎∃𝑏(𝑝 = 〈𝑎, 𝑏〉 ∧ 𝜓)) |