Step | Hyp | Ref
| Expression |
1 | | f1osng 6874 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → {⟨𝐴, 𝐴⟩}:{𝐴}–1-1-onto→{𝐴}) |
2 | 1 | anidms 567 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → {⟨𝐴, 𝐴⟩}:{𝐴}–1-1-onto→{𝐴}) |
3 | 2 | ad2antrr 724 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 = 𝐵) → {⟨𝐴, 𝐴⟩}:{𝐴}–1-1-onto→{𝐴}) |
4 | | dfsn2 4641 |
. . . . . 6
⊢
{⟨𝐴, 𝐴⟩} = {⟨𝐴, 𝐴⟩, ⟨𝐴, 𝐴⟩} |
5 | | opeq2 4874 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐴⟩ = ⟨𝐴, 𝐵⟩) |
6 | | opeq1 4873 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐴⟩ = ⟨𝐵, 𝐴⟩) |
7 | 5, 6 | preq12d 4745 |
. . . . . 6
⊢ (𝐴 = 𝐵 → {⟨𝐴, 𝐴⟩, ⟨𝐴, 𝐴⟩} = {⟨𝐴, 𝐵⟩, ⟨𝐵, 𝐴⟩}) |
8 | 4, 7 | eqtrid 2784 |
. . . . 5
⊢ (𝐴 = 𝐵 → {⟨𝐴, 𝐴⟩} = {⟨𝐴, 𝐵⟩, ⟨𝐵, 𝐴⟩}) |
9 | | dfsn2 4641 |
. . . . . 6
⊢ {𝐴} = {𝐴, 𝐴} |
10 | | preq2 4738 |
. . . . . 6
⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵}) |
11 | 9, 10 | eqtrid 2784 |
. . . . 5
⊢ (𝐴 = 𝐵 → {𝐴} = {𝐴, 𝐵}) |
12 | 8, 11, 11 | f1oeq123d 6827 |
. . . 4
⊢ (𝐴 = 𝐵 → ({⟨𝐴, 𝐴⟩}:{𝐴}–1-1-onto→{𝐴} ↔ {⟨𝐴, 𝐵⟩, ⟨𝐵, 𝐴⟩}:{𝐴, 𝐵}–1-1-onto→{𝐴, 𝐵})) |
13 | 12 | adantl 482 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 = 𝐵) → ({⟨𝐴, 𝐴⟩}:{𝐴}–1-1-onto→{𝐴} ↔ {⟨𝐴, 𝐵⟩, ⟨𝐵, 𝐴⟩}:{𝐴, 𝐵}–1-1-onto→{𝐴, 𝐵})) |
14 | 3, 13 | mpbid 231 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 = 𝐵) → {⟨𝐴, 𝐵⟩, ⟨𝐵, 𝐴⟩}:{𝐴, 𝐵}–1-1-onto→{𝐴, 𝐵}) |
15 | | simpll 765 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ 𝑉) |
16 | | simplr 767 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ 𝑊) |
17 | | simpr 485 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → 𝐴 ≠ 𝐵) |
18 | | fnprg 6607 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {⟨𝐴, 𝐵⟩, ⟨𝐵, 𝐴⟩} Fn {𝐴, 𝐵}) |
19 | 15, 16, 16, 15, 17, 18 | syl221anc 1381 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → {⟨𝐴, 𝐵⟩, ⟨𝐵, 𝐴⟩} Fn {𝐴, 𝐵}) |
20 | | cnvsng 6222 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ◡{⟨𝐴, 𝐵⟩} = {⟨𝐵, 𝐴⟩}) |
21 | | cnvsng 6222 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → ◡{⟨𝐵, 𝐴⟩} = {⟨𝐴, 𝐵⟩}) |
22 | 21 | ancoms 459 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ◡{⟨𝐵, 𝐴⟩} = {⟨𝐴, 𝐵⟩}) |
23 | 20, 22 | uneq12d 4164 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (◡{⟨𝐴, 𝐵⟩} ∪ ◡{⟨𝐵, 𝐴⟩}) = ({⟨𝐵, 𝐴⟩} ∪ {⟨𝐴, 𝐵⟩})) |
24 | | uncom 4153 |
. . . . . . . 8
⊢
({⟨𝐵, 𝐴⟩} ∪ {⟨𝐴, 𝐵⟩}) = ({⟨𝐴, 𝐵⟩} ∪ {⟨𝐵, 𝐴⟩}) |
25 | 23, 24 | eqtrdi 2788 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (◡{⟨𝐴, 𝐵⟩} ∪ ◡{⟨𝐵, 𝐴⟩}) = ({⟨𝐴, 𝐵⟩} ∪ {⟨𝐵, 𝐴⟩})) |
26 | 25 | adantr 481 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → (◡{⟨𝐴, 𝐵⟩} ∪ ◡{⟨𝐵, 𝐴⟩}) = ({⟨𝐴, 𝐵⟩} ∪ {⟨𝐵, 𝐴⟩})) |
27 | | df-pr 4631 |
. . . . . . . 8
⊢
{⟨𝐴, 𝐵⟩, ⟨𝐵, 𝐴⟩} = ({⟨𝐴, 𝐵⟩} ∪ {⟨𝐵, 𝐴⟩}) |
28 | 27 | cnveqi 5874 |
. . . . . . 7
⊢ ◡{⟨𝐴, 𝐵⟩, ⟨𝐵, 𝐴⟩} = ◡({⟨𝐴, 𝐵⟩} ∪ {⟨𝐵, 𝐴⟩}) |
29 | | cnvun 6142 |
. . . . . . 7
⊢ ◡({⟨𝐴, 𝐵⟩} ∪ {⟨𝐵, 𝐴⟩}) = (◡{⟨𝐴, 𝐵⟩} ∪ ◡{⟨𝐵, 𝐴⟩}) |
30 | 28, 29 | eqtri 2760 |
. . . . . 6
⊢ ◡{⟨𝐴, 𝐵⟩, ⟨𝐵, 𝐴⟩} = (◡{⟨𝐴, 𝐵⟩} ∪ ◡{⟨𝐵, 𝐴⟩}) |
31 | 26, 30, 27 | 3eqtr4g 2797 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → ◡{⟨𝐴, 𝐵⟩, ⟨𝐵, 𝐴⟩} = {⟨𝐴, 𝐵⟩, ⟨𝐵, 𝐴⟩}) |
32 | 31 | fneq1d 6642 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → (◡{⟨𝐴, 𝐵⟩, ⟨𝐵, 𝐴⟩} Fn {𝐴, 𝐵} ↔ {⟨𝐴, 𝐵⟩, ⟨𝐵, 𝐴⟩} Fn {𝐴, 𝐵})) |
33 | 19, 32 | mpbird 256 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → ◡{⟨𝐴, 𝐵⟩, ⟨𝐵, 𝐴⟩} Fn {𝐴, 𝐵}) |
34 | | dff1o4 6841 |
. . 3
⊢
({⟨𝐴, 𝐵⟩, ⟨𝐵, 𝐴⟩}:{𝐴, 𝐵}–1-1-onto→{𝐴, 𝐵} ↔ ({⟨𝐴, 𝐵⟩, ⟨𝐵, 𝐴⟩} Fn {𝐴, 𝐵} ∧ ◡{⟨𝐴, 𝐵⟩, ⟨𝐵, 𝐴⟩} Fn {𝐴, 𝐵})) |
35 | 19, 33, 34 | sylanbrc 583 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → {⟨𝐴, 𝐵⟩, ⟨𝐵, 𝐴⟩}:{𝐴, 𝐵}–1-1-onto→{𝐴, 𝐵}) |
36 | 14, 35 | pm2.61dane 3029 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {⟨𝐴, 𝐵⟩, ⟨𝐵, 𝐴⟩}:{𝐴, 𝐵}–1-1-onto→{𝐴, 𝐵}) |