Proof of Theorem copsex2b
| Step | Hyp | Ref
| Expression |
| 1 | | eqcom 2744 |
. . . . . . 7
⊢
(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ↔ 〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉) |
| 2 | | vex 3484 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
| 3 | | vex 3484 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
| 4 | 2, 3 | opth 5481 |
. . . . . . 7
⊢
(〈𝑥, 𝑦〉 = 〈𝐴, 𝐵〉 ↔ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) |
| 5 | 1, 4 | bitri 275 |
. . . . . 6
⊢
(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ↔ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) |
| 6 | | eqvisset 3500 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → 𝐴 ∈ V) |
| 7 | | eqvisset 3500 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → 𝐵 ∈ V) |
| 8 | 6, 7 | anim12i 613 |
. . . . . 6
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
| 9 | 5, 8 | sylbi 217 |
. . . . 5
⊢
(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
| 10 | 9 | adantr 480 |
. . . 4
⊢
((〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
| 11 | 10 | exlimivv 1932 |
. . 3
⊢
(∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
| 12 | 11 | anim2i 617 |
. 2
⊢ ((𝜑 ∧ ∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓)) → (𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V))) |
| 13 | | simpl 482 |
. . 3
⊢ (((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
| 14 | 13 | anim2i 617 |
. 2
⊢ ((𝜑 ∧ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒)) → (𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V))) |
| 15 | | copsex2b.xph |
. . . . 5
⊢ (𝜑 → ∀𝑥𝜑) |
| 16 | | ax-5 1910 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ∀𝑥(𝐴 ∈ V ∧ 𝐵 ∈ V)) |
| 17 | 15, 16 | hban 2300 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → ∀𝑥(𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V))) |
| 18 | | copsex2b.yph |
. . . . 5
⊢ (𝜑 → ∀𝑦𝜑) |
| 19 | | ax-5 1910 |
. . . . 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 771 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → 𝐴 ∈ V) |
| 26 | | simprr 773 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → 𝐵 ∈ V) |
| 27 | | copsex2b.is |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) |
| 28 | 27 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) ∧ (𝑥 = 𝐴 ∧ 𝑦 = 𝐵)) → (𝜓 ↔ 𝜒)) |
| 29 | 17, 20, 22, 24, 25, 26, 28 | copsex2d 37140 |
. . 3
⊢ ((𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ 𝜒)) |
| 30 | | ibar 528 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝜒 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒))) |
| 31 | 30 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → (𝜒 ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒))) |
| 32 | 29, 31 | bitrd 279 |
. 2
⊢ ((𝜑 ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V)) → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒))) |
| 33 | 12, 14, 32 | pm5.21nd 802 |
1
⊢ (𝜑 → (∃𝑥∃𝑦(〈𝐴, 𝐵〉 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝜒))) |