Proof of Theorem copsex2d
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | copsex2d.exa | . . 3
⊢ (𝜑 → 𝐴 ∈ 𝑈) | 
| 2 |  | elisset 2823 | . . 3
⊢ (𝐴 ∈ 𝑈 → ∃𝑥 𝑥 = 𝐴) | 
| 3 | 1, 2 | syl 17 | . 2
⊢ (𝜑 → ∃𝑥 𝑥 = 𝐴) | 
| 4 |  | copsex2d.exb | . . 3
⊢ (𝜑 → 𝐵 ∈ 𝑉) | 
| 5 |  | elisset 2823 | . . 3
⊢ (𝐵 ∈ 𝑉 → ∃𝑦 𝑦 = 𝐵) | 
| 6 | 4, 5 | syl 17 | . 2
⊢ (𝜑 → ∃𝑦 𝑦 = 𝐵) | 
| 7 |  | exdistrv 1955 | . . 3
⊢
(∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)) | 
| 8 |  | copsex2d.xph | . . . 4
⊢ (𝜑 → ∀𝑥𝜑) | 
| 9 |  | nfe1 2150 | . . . . . . 7
⊢
Ⅎ𝑥∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) | 
| 10 | 9 | a1i 11 | . . . . . 6
⊢ (𝜑 → Ⅎ𝑥∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓)) | 
| 11 |  | copsex2d.xch | . . . . . 6
⊢ (𝜑 → Ⅎ𝑥𝜒) | 
| 12 | 10, 11 | nfbid 1902 | . . . . 5
⊢ (𝜑 → Ⅎ𝑥(∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ 𝜒)) | 
| 13 | 12 | 19.9d 2203 | . . . 4
⊢ (𝜑 → (∃𝑥(∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ 𝜒) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ 𝜒))) | 
| 14 |  | copsex2d.yph | . . . . 5
⊢ (𝜑 → ∀𝑦𝜑) | 
| 15 |  | nfe1 2150 | . . . . . . . . 9
⊢
Ⅎ𝑦∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) | 
| 16 | 15 | a1i 11 | . . . . . . . 8
⊢ (𝜑 → Ⅎ𝑦∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓)) | 
| 17 | 8, 16 | bj-nfexd 37139 | . . . . . . 7
⊢ (𝜑 → Ⅎ𝑦∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓)) | 
| 18 |  | copsex2d.ych | . . . . . . 7
⊢ (𝜑 → Ⅎ𝑦𝜒) | 
| 19 | 17, 18 | nfbid 1902 | . . . . . 6
⊢ (𝜑 → Ⅎ𝑦(∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ 𝜒)) | 
| 20 | 19 | 19.9d 2203 | . . . . 5
⊢ (𝜑 → (∃𝑦(∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ 𝜒) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ 𝜒))) | 
| 21 |  | opeq12 4875 | . . . . . . . . 9
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → 〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉) | 
| 22 |  | copsexgw 5495 | . . . . . . . . . . 11
⊢
(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 → (𝜓 ↔ ∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓))) | 
| 23 | 22 | bicomd 223 | . . . . . . . . . 10
⊢
(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ 𝜓)) | 
| 24 | 23 | eqcoms 2745 | . . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉 → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ 𝜓)) | 
| 25 | 21, 24 | syl 17 | . . . . . . . 8
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ 𝜓)) | 
| 26 | 25 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ 𝜓)) | 
| 27 |  | copsex2d.is | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) | 
| 28 | 26, 27 | bitrd 279 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ 𝜒)) | 
| 29 | 28 | ex 412 | . . . . 5
⊢ (𝜑 → ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ 𝜒))) | 
| 30 | 14, 20, 29 | bj-exlimd 36626 | . . . 4
⊢ (𝜑 → (∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ 𝜒))) | 
| 31 | 8, 13, 30 | bj-exlimd 36626 | . . 3
⊢ (𝜑 → (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ 𝜒))) | 
| 32 | 7, 31 | biimtrrid 243 | . 2
⊢ (𝜑 → ((∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ 𝜒))) | 
| 33 | 3, 6, 32 | mp2and 699 | 1
⊢ (𝜑 → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ 𝜒)) |