Proof of Theorem elpr2elpr
Step | Hyp | Ref
| Expression |
1 | | elpri 4145 |
. . . 4
⊢ (𝐴 ∈ {𝑋, 𝑌} → (𝐴 = 𝑋 ∨ 𝐴 = 𝑌)) |
2 | | simprr 792 |
. . . . . . 7
⊢ ((𝐴 = 𝑋 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → 𝑌 ∈ 𝑉) |
3 | | preq2 4213 |
. . . . . . . . 9
⊢ (𝑏 = 𝑌 → {𝐴, 𝑏} = {𝐴, 𝑌}) |
4 | 3 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑏 = 𝑌 → ({𝑋, 𝑌} = {𝐴, 𝑏} ↔ {𝑋, 𝑌} = {𝐴, 𝑌})) |
5 | 4 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 = 𝑋 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑏 = 𝑌) → ({𝑋, 𝑌} = {𝐴, 𝑏} ↔ {𝑋, 𝑌} = {𝐴, 𝑌})) |
6 | | preq1 4212 |
. . . . . . . . 9
⊢ (𝑋 = 𝐴 → {𝑋, 𝑌} = {𝐴, 𝑌}) |
7 | 6 | eqcoms 2618 |
. . . . . . . 8
⊢ (𝐴 = 𝑋 → {𝑋, 𝑌} = {𝐴, 𝑌}) |
8 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 = 𝑋 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → {𝑋, 𝑌} = {𝐴, 𝑌}) |
9 | 2, 5, 8 | rspcedvd 3289 |
. . . . . 6
⊢ ((𝐴 = 𝑋 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ∃𝑏 ∈ 𝑉 {𝑋, 𝑌} = {𝐴, 𝑏}) |
10 | 9 | ex 449 |
. . . . 5
⊢ (𝐴 = 𝑋 → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ∃𝑏 ∈ 𝑉 {𝑋, 𝑌} = {𝐴, 𝑏})) |
11 | | simprl 790 |
. . . . . . 7
⊢ ((𝐴 = 𝑌 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → 𝑋 ∈ 𝑉) |
12 | | preq2 4213 |
. . . . . . . . 9
⊢ (𝑏 = 𝑋 → {𝐴, 𝑏} = {𝐴, 𝑋}) |
13 | 12 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑏 = 𝑋 → ({𝑋, 𝑌} = {𝐴, 𝑏} ↔ {𝑋, 𝑌} = {𝐴, 𝑋})) |
14 | 13 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 = 𝑌 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ 𝑏 = 𝑋) → ({𝑋, 𝑌} = {𝐴, 𝑏} ↔ {𝑋, 𝑌} = {𝐴, 𝑋})) |
15 | | preq2 4213 |
. . . . . . . . . 10
⊢ (𝑌 = 𝐴 → {𝑋, 𝑌} = {𝑋, 𝐴}) |
16 | 15 | eqcoms 2618 |
. . . . . . . . 9
⊢ (𝐴 = 𝑌 → {𝑋, 𝑌} = {𝑋, 𝐴}) |
17 | | prcom 4211 |
. . . . . . . . 9
⊢ {𝑋, 𝐴} = {𝐴, 𝑋} |
18 | 16, 17 | syl6eq 2660 |
. . . . . . . 8
⊢ (𝐴 = 𝑌 → {𝑋, 𝑌} = {𝐴, 𝑋}) |
19 | 18 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 = 𝑌 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → {𝑋, 𝑌} = {𝐴, 𝑋}) |
20 | 11, 14, 19 | rspcedvd 3289 |
. . . . . 6
⊢ ((𝐴 = 𝑌 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → ∃𝑏 ∈ 𝑉 {𝑋, 𝑌} = {𝐴, 𝑏}) |
21 | 20 | ex 449 |
. . . . 5
⊢ (𝐴 = 𝑌 → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ∃𝑏 ∈ 𝑉 {𝑋, 𝑌} = {𝐴, 𝑏})) |
22 | 10, 21 | jaoi 393 |
. . . 4
⊢ ((𝐴 = 𝑋 ∨ 𝐴 = 𝑌) → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ∃𝑏 ∈ 𝑉 {𝑋, 𝑌} = {𝐴, 𝑏})) |
23 | 1, 22 | syl 17 |
. . 3
⊢ (𝐴 ∈ {𝑋, 𝑌} → ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ∃𝑏 ∈ 𝑉 {𝑋, 𝑌} = {𝐴, 𝑏})) |
24 | 23 | com12 32 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝐴 ∈ {𝑋, 𝑌} → ∃𝑏 ∈ 𝑉 {𝑋, 𝑌} = {𝐴, 𝑏})) |
25 | 24 | 3impia 1253 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝐴 ∈ {𝑋, 𝑌}) → ∃𝑏 ∈ 𝑉 {𝑋, 𝑌} = {𝐴, 𝑏}) |