Proof of Theorem f1oprswap
| Step | Hyp | Ref
| Expression |
| 1 | | f1osng 6889 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → {〈𝐴, 𝐴〉}:{𝐴}–1-1-onto→{𝐴}) |
| 2 | 1 | anidms 566 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → {〈𝐴, 𝐴〉}:{𝐴}–1-1-onto→{𝐴}) |
| 3 | 2 | ad2antrr 726 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 = 𝐵) → {〈𝐴, 𝐴〉}:{𝐴}–1-1-onto→{𝐴}) |
| 4 | | dfsn2 4639 |
. . . . . 6
⊢
{〈𝐴, 𝐴〉} = {〈𝐴, 𝐴〉, 〈𝐴, 𝐴〉} |
| 5 | | opeq2 4874 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐴〉 = 〈𝐴, 𝐵〉) |
| 6 | | opeq1 4873 |
. . . . . . 7
⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐴〉 = 〈𝐵, 𝐴〉) |
| 7 | 5, 6 | preq12d 4741 |
. . . . . 6
⊢ (𝐴 = 𝐵 → {〈𝐴, 𝐴〉, 〈𝐴, 𝐴〉} = {〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉}) |
| 8 | 4, 7 | eqtrid 2789 |
. . . . 5
⊢ (𝐴 = 𝐵 → {〈𝐴, 𝐴〉} = {〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉}) |
| 9 | | dfsn2 4639 |
. . . . . 6
⊢ {𝐴} = {𝐴, 𝐴} |
| 10 | | preq2 4734 |
. . . . . 6
⊢ (𝐴 = 𝐵 → {𝐴, 𝐴} = {𝐴, 𝐵}) |
| 11 | 9, 10 | eqtrid 2789 |
. . . . 5
⊢ (𝐴 = 𝐵 → {𝐴} = {𝐴, 𝐵}) |
| 12 | 8, 11, 11 | f1oeq123d 6842 |
. . . 4
⊢ (𝐴 = 𝐵 → ({〈𝐴, 𝐴〉}:{𝐴}–1-1-onto→{𝐴} ↔ {〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉}:{𝐴, 𝐵}–1-1-onto→{𝐴, 𝐵})) |
| 13 | 12 | adantl 481 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 = 𝐵) → ({〈𝐴, 𝐴〉}:{𝐴}–1-1-onto→{𝐴} ↔ {〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉}:{𝐴, 𝐵}–1-1-onto→{𝐴, 𝐵})) |
| 14 | 3, 13 | mpbid 232 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 = 𝐵) → {〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉}:{𝐴, 𝐵}–1-1-onto→{𝐴, 𝐵}) |
| 15 | | simpll 767 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ 𝑉) |
| 16 | | simplr 769 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ 𝑊) |
| 17 | | simpr 484 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → 𝐴 ≠ 𝐵) |
| 18 | | fnprg 6625 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → {〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉} Fn {𝐴, 𝐵}) |
| 19 | 15, 16, 16, 15, 17, 18 | syl221anc 1383 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → {〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉} Fn {𝐴, 𝐵}) |
| 20 | | cnvsng 6243 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ◡{〈𝐴, 𝐵〉} = {〈𝐵, 𝐴〉}) |
| 21 | | cnvsng 6243 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → ◡{〈𝐵, 𝐴〉} = {〈𝐴, 𝐵〉}) |
| 22 | 21 | ancoms 458 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ◡{〈𝐵, 𝐴〉} = {〈𝐴, 𝐵〉}) |
| 23 | 20, 22 | uneq12d 4169 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (◡{〈𝐴, 𝐵〉} ∪ ◡{〈𝐵, 𝐴〉}) = ({〈𝐵, 𝐴〉} ∪ {〈𝐴, 𝐵〉})) |
| 24 | | uncom 4158 |
. . . . . . . 8
⊢
({〈𝐵, 𝐴〉} ∪ {〈𝐴, 𝐵〉}) = ({〈𝐴, 𝐵〉} ∪ {〈𝐵, 𝐴〉}) |
| 25 | 23, 24 | eqtrdi 2793 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (◡{〈𝐴, 𝐵〉} ∪ ◡{〈𝐵, 𝐴〉}) = ({〈𝐴, 𝐵〉} ∪ {〈𝐵, 𝐴〉})) |
| 26 | 25 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → (◡{〈𝐴, 𝐵〉} ∪ ◡{〈𝐵, 𝐴〉}) = ({〈𝐴, 𝐵〉} ∪ {〈𝐵, 𝐴〉})) |
| 27 | | df-pr 4629 |
. . . . . . . 8
⊢
{〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉} = ({〈𝐴, 𝐵〉} ∪ {〈𝐵, 𝐴〉}) |
| 28 | 27 | cnveqi 5885 |
. . . . . . 7
⊢ ◡{〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉} = ◡({〈𝐴, 𝐵〉} ∪ {〈𝐵, 𝐴〉}) |
| 29 | | cnvun 6162 |
. . . . . . 7
⊢ ◡({〈𝐴, 𝐵〉} ∪ {〈𝐵, 𝐴〉}) = (◡{〈𝐴, 𝐵〉} ∪ ◡{〈𝐵, 𝐴〉}) |
| 30 | 28, 29 | eqtri 2765 |
. . . . . 6
⊢ ◡{〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉} = (◡{〈𝐴, 𝐵〉} ∪ ◡{〈𝐵, 𝐴〉}) |
| 31 | 26, 30, 27 | 3eqtr4g 2802 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → ◡{〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉} = {〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉}) |
| 32 | 31 | fneq1d 6661 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → (◡{〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉} Fn {𝐴, 𝐵} ↔ {〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉} Fn {𝐴, 𝐵})) |
| 33 | 19, 32 | mpbird 257 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 ≠ 𝐵) → ◡{〈𝐴, 𝐵〉, 〈𝐵, 𝐴〉} Fn {𝐴, 𝐵}) |
| 34 | | dff1o4 6856 |
. . 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→{𝐴, 𝐵}) |