Step | Hyp | Ref
| Expression |
1 | | sprel 44609 |
. . 3
⊢ ({𝑋, 𝑌} ∈ (Pairs‘𝑉) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 {𝑋, 𝑌} = {𝑎, 𝑏}) |
2 | | preq12bg 4764 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ({𝑋, 𝑌} = {𝑎, 𝑏} ↔ ((𝑋 = 𝑎 ∧ 𝑌 = 𝑏) ∨ (𝑋 = 𝑏 ∧ 𝑌 = 𝑎)))) |
3 | | eleq1 2825 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑋 → (𝑎 ∈ 𝑉 ↔ 𝑋 ∈ 𝑉)) |
4 | 3 | eqcoms 2745 |
. . . . . . . . . . . 12
⊢ (𝑋 = 𝑎 → (𝑎 ∈ 𝑉 ↔ 𝑋 ∈ 𝑉)) |
5 | | eleq1 2825 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝑌 → (𝑏 ∈ 𝑉 ↔ 𝑌 ∈ 𝑉)) |
6 | 5 | eqcoms 2745 |
. . . . . . . . . . . 12
⊢ (𝑌 = 𝑏 → (𝑏 ∈ 𝑉 ↔ 𝑌 ∈ 𝑉)) |
7 | 4, 6 | bi2anan9 639 |
. . . . . . . . . . 11
⊢ ((𝑋 = 𝑎 ∧ 𝑌 = 𝑏) → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ↔ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉))) |
8 | 7 | biimpd 232 |
. . . . . . . . . 10
⊢ ((𝑋 = 𝑎 ∧ 𝑌 = 𝑏) → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉))) |
9 | | eleq1 2825 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑋 → (𝑏 ∈ 𝑉 ↔ 𝑋 ∈ 𝑉)) |
10 | 9 | eqcoms 2745 |
. . . . . . . . . . . . 13
⊢ (𝑋 = 𝑏 → (𝑏 ∈ 𝑉 ↔ 𝑋 ∈ 𝑉)) |
11 | | eleq1 2825 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑌 → (𝑎 ∈ 𝑉 ↔ 𝑌 ∈ 𝑉)) |
12 | 11 | eqcoms 2745 |
. . . . . . . . . . . . 13
⊢ (𝑌 = 𝑎 → (𝑎 ∈ 𝑉 ↔ 𝑌 ∈ 𝑉)) |
13 | 10, 12 | bi2anan9 639 |
. . . . . . . . . . . 12
⊢ ((𝑋 = 𝑏 ∧ 𝑌 = 𝑎) → ((𝑏 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉) ↔ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉))) |
14 | 13 | biimpd 232 |
. . . . . . . . . . 11
⊢ ((𝑋 = 𝑏 ∧ 𝑌 = 𝑎) → ((𝑏 ∈ 𝑉 ∧ 𝑎 ∈ 𝑉) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉))) |
15 | 14 | ancomsd 469 |
. . . . . . . . . 10
⊢ ((𝑋 = 𝑏 ∧ 𝑌 = 𝑎) → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉))) |
16 | 8, 15 | jaoi 857 |
. . . . . . . . 9
⊢ (((𝑋 = 𝑎 ∧ 𝑌 = 𝑏) ∨ (𝑋 = 𝑏 ∧ 𝑌 = 𝑎)) → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉))) |
17 | 16 | com12 32 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → (((𝑋 = 𝑎 ∧ 𝑌 = 𝑏) ∨ (𝑋 = 𝑏 ∧ 𝑌 = 𝑎)) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉))) |
18 | 17 | adantl 485 |
. . . . . . 7
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (((𝑋 = 𝑎 ∧ 𝑌 = 𝑏) ∨ (𝑋 = 𝑏 ∧ 𝑌 = 𝑎)) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉))) |
19 | 2, 18 | sylbid 243 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊) ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ({𝑋, 𝑌} = {𝑎, 𝑏} → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉))) |
20 | 19 | expcom 417 |
. . . . 5
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊) → ({𝑋, 𝑌} = {𝑎, 𝑏} → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)))) |
21 | 20 | com23 86 |
. . . 4
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → ({𝑋, 𝑌} = {𝑎, 𝑏} → ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)))) |
22 | 21 | rexlimivv 3211 |
. . 3
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 {𝑋, 𝑌} = {𝑎, 𝑏} → ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉))) |
23 | 1, 22 | syl 17 |
. 2
⊢ ({𝑋, 𝑌} ∈ (Pairs‘𝑉) → ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉))) |
24 | 23 | imp 410 |
1
⊢ (({𝑋, 𝑌} ∈ (Pairs‘𝑉) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊)) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) |