Proof of Theorem f1oprswap
Step | Hyp | Ref
| Expression |
1 | | f1osng 6670 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → {〈𝐴, 𝐴〉}:{𝐴}–1-1-onto→{𝐴}) |
2 | 1 | anidms 570 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → {〈𝐴, 𝐴〉}:{𝐴}–1-1-onto→{𝐴}) |
3 | 2 | ad2antrr 726 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 = 𝐵) → {〈𝐴, 𝐴〉}:{𝐴}–1-1-onto→{𝐴}) |
4 | | dfsn2 4539 |
. . . . . 6
⊢
{〈𝐴, 𝐴〉} = {〈𝐴, 𝐴〉, 〈𝐴, 𝐴〉} |
5 | | opeq2 4771 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐴〉 = 〈𝐴, 𝐵〉) |
6 | | opeq1 4769 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐴〉 = 〈𝐵, 𝐴〉) |
7 | 5, 6 | preq12d 4642 |
. . . . . 6
⊢ (𝐴 = 𝐵 → {〈𝐴, 𝐴〉, 〈𝐴, 𝐴〉} = {〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉}) |
8 | 4, 7 | syl5eq 2786 |
. . . . 5
⊢ (𝐴 = 𝐵 → {〈𝐴, 𝐴〉} = {〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉}) |
9 | | dfsn2 4539 |
. . . . . 6
⊢ {𝐴} = {𝐴, 𝐴} |
10 | | preq2 4635 |
. . . . . 6
⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵}) |
11 | 9, 10 | syl5eq 2786 |
. . . . 5
⊢ (𝐴 = 𝐵 → {𝐴} = {𝐴, 𝐵}) |
12 | 8, 11, 11 | f1oeq123d 6624 |
. . . 4
⊢ (𝐴 = 𝐵 → ({〈𝐴, 𝐴〉}:{𝐴}–1-1-onto→{𝐴} ↔ {〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉}:{𝐴, 𝐵}–1-1-onto→{𝐴, 𝐵})) |
13 | 12 | adantl 485 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 = 𝐵) → ({〈𝐴, 𝐴〉}:{𝐴}–1-1-onto→{𝐴} ↔ {〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉}:{𝐴, 𝐵}–1-1-onto→{𝐴, 𝐵})) |
14 | 3, 13 | mpbid 235 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 = 𝐵) → {〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉}:{𝐴, 𝐵}–1-1-onto→{𝐴, 𝐵}) |
15 | | simpll 767 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ 𝑉) |
16 | | simplr 769 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ 𝑊) |
17 | | simpr 488 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → 𝐴 ≠ 𝐵) |
18 | | fnprg 6408 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉} Fn {𝐴, 𝐵}) |
19 | 15, 16, 16, 15, 17, 18 | syl221anc 1382 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → {〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉} Fn {𝐴, 𝐵}) |
20 | | cnvsng 6065 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ◡{〈𝐴, 𝐵〉} = {〈𝐵, 𝐴〉}) |
21 | | cnvsng 6065 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → ◡{〈𝐵, 𝐴〉} = {〈𝐴, 𝐵〉}) |
22 | 21 | ancoms 462 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ◡{〈𝐵, 𝐴〉} = {〈𝐴, 𝐵〉}) |
23 | 20, 22 | uneq12d 4064 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (◡{〈𝐴, 𝐵〉} ∪ ◡{〈𝐵, 𝐴〉}) = ({〈𝐵, 𝐴〉} ∪ {〈𝐴, 𝐵〉})) |
24 | | uncom 4053 |
. . . . . . . 8
⊢
({〈𝐵, 𝐴〉} ∪ {〈𝐴, 𝐵〉}) = ({〈𝐴, 𝐵〉} ∪ {〈𝐵, 𝐴〉}) |
25 | 23, 24 | eqtrdi 2790 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (◡{〈𝐴, 𝐵〉} ∪ ◡{〈𝐵, 𝐴〉}) = ({〈𝐴, 𝐵〉} ∪ {〈𝐵, 𝐴〉})) |
26 | 25 | adantr 484 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → (◡{〈𝐴, 𝐵〉} ∪ ◡{〈𝐵, 𝐴〉}) = ({〈𝐴, 𝐵〉} ∪ {〈𝐵, 𝐴〉})) |
27 | | df-pr 4529 |
. . . . . . . 8
⊢
{〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉} = ({〈𝐴, 𝐵〉} ∪ {〈𝐵, 𝐴〉}) |
28 | 27 | cnveqi 5727 |
. . . . . . 7
⊢ ◡{〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉} = ◡({〈𝐴, 𝐵〉} ∪ {〈𝐵, 𝐴〉}) |
29 | | cnvun 5985 |
. . . . . . 7
⊢ ◡({〈𝐴, 𝐵〉} ∪ {〈𝐵, 𝐴〉}) = (◡{〈𝐴, 𝐵〉} ∪ ◡{〈𝐵, 𝐴〉}) |
30 | 28, 29 | eqtri 2762 |
. . . . . 6
⊢ ◡{〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉} = (◡{〈𝐴, 𝐵〉} ∪ ◡{〈𝐵, 𝐴〉}) |
31 | 26, 30, 27 | 3eqtr4g 2799 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → ◡{〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉} = {〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉}) |
32 | 31 | fneq1d 6441 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → (◡{〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉} Fn {𝐴, 𝐵} ↔ {〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉} Fn {𝐴, 𝐵})) |
33 | 19, 32 | mpbird 260 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → ◡{〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉} Fn {𝐴, 𝐵}) |
34 | | dff1o4 6638 |
. . 3
⊢
({〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉}:{𝐴, 𝐵}–1-1-onto→{𝐴, 𝐵} ↔ ({〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉} Fn {𝐴, 𝐵} ∧ ◡{〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉} Fn {𝐴, 𝐵})) |
35 | 19, 33, 34 | sylanbrc 586 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → {〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉}:{𝐴, 𝐵}–1-1-onto→{𝐴, 𝐵}) |
36 | 14, 35 | pm2.61dane 3022 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → {〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉}:{𝐴, 𝐵}–1-1-onto→{𝐴, 𝐵}) |