Proof of Theorem f1ofvswap
| Step | Hyp | Ref
| Expression |
| 1 | | f1oi 6886 |
. . . . . 6
⊢ ( I
↾ (𝐴 ∖ {𝑋, 𝑌})):(𝐴 ∖ {𝑋, 𝑌})–1-1-onto→(𝐴 ∖ {𝑋, 𝑌}) |
| 2 | | f1oprswap 6892 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}:{𝑋, 𝑌}–1-1-onto→{𝑋, 𝑌}) |
| 3 | | disjdifr 4473 |
. . . . . . 7
⊢ ((𝐴 ∖ {𝑋, 𝑌}) ∩ {𝑋, 𝑌}) = ∅ |
| 4 | | f1oun 6867 |
. . . . . . 7
⊢ (((( I
↾ (𝐴 ∖ {𝑋, 𝑌})):(𝐴 ∖ {𝑋, 𝑌})–1-1-onto→(𝐴 ∖ {𝑋, 𝑌}) ∧ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}:{𝑋, 𝑌}–1-1-onto→{𝑋, 𝑌}) ∧ (((𝐴 ∖ {𝑋, 𝑌}) ∩ {𝑋, 𝑌}) = ∅ ∧ ((𝐴 ∖ {𝑋, 𝑌}) ∩ {𝑋, 𝑌}) = ∅)) → (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}):((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌})–1-1-onto→((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌})) |
| 5 | 3, 3, 4 | mpanr12 705 |
. . . . . 6
⊢ ((( I
↾ (𝐴 ∖ {𝑋, 𝑌})):(𝐴 ∖ {𝑋, 𝑌})–1-1-onto→(𝐴 ∖ {𝑋, 𝑌}) ∧ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}:{𝑋, 𝑌}–1-1-onto→{𝑋, 𝑌}) → (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}):((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌})–1-1-onto→((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌})) |
| 6 | 1, 2, 5 | sylancr 587 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}):((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌})–1-1-onto→((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌})) |
| 7 | | prssi 4821 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → {𝑋, 𝑌} ⊆ 𝐴) |
| 8 | | undifr 4483 |
. . . . . . 7
⊢ ({𝑋, 𝑌} ⊆ 𝐴 ↔ ((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌}) = 𝐴) |
| 9 | 7, 8 | sylib 218 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌}) = 𝐴) |
| 10 | | f1oeq23 6839 |
. . . . . 6
⊢ ((((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌}) = 𝐴 ∧ ((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌}) = 𝐴) → ((( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}):((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌})–1-1-onto→((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌}) ↔ (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}):𝐴–1-1-onto→𝐴)) |
| 11 | 9, 9, 10 | syl2anc 584 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}):((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌})–1-1-onto→((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌}) ↔ (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}):𝐴–1-1-onto→𝐴)) |
| 12 | 6, 11 | mpbid 232 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}):𝐴–1-1-onto→𝐴) |
| 13 | | f1oco 6871 |
. . . 4
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}):𝐴–1-1-onto→𝐴) → (𝐹 ∘ (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉})):𝐴–1-1-onto→𝐵) |
| 14 | 12, 13 | sylan2 593 |
. . 3
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → (𝐹 ∘ (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉})):𝐴–1-1-onto→𝐵) |
| 15 | 14 | 3impb 1115 |
. 2
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉})):𝐴–1-1-onto→𝐵) |
| 16 | | f1ofn 6849 |
. . . 4
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴) |
| 17 | | coundi 6267 |
. . . . . 6
⊢ (𝐹 ∘ (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉})) = ((𝐹 ∘ ( I ↾ (𝐴 ∖ {𝑋, 𝑌}))) ∪ (𝐹 ∘ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉})) |
| 18 | | fcoconst 7154 |
. . . . . . . . . . 11
⊢ ((𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ ({𝑋} × {𝑌})) = ({𝑋} × {(𝐹‘𝑌)})) |
| 19 | 18 | 3adant2 1132 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ ({𝑋} × {𝑌})) = ({𝑋} × {(𝐹‘𝑌)})) |
| 20 | | xpsng 7159 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ({𝑋} × {𝑌}) = {〈𝑋, 𝑌〉}) |
| 21 | 20 | coeq2d 5873 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ ({𝑋} × {𝑌})) = (𝐹 ∘ {〈𝑋, 𝑌〉})) |
| 22 | 21 | 3adant1 1131 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ ({𝑋} × {𝑌})) = (𝐹 ∘ {〈𝑋, 𝑌〉})) |
| 23 | | fvex 6919 |
. . . . . . . . . . . 12
⊢ (𝐹‘𝑌) ∈ V |
| 24 | | xpsng 7159 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝐴 ∧ (𝐹‘𝑌) ∈ V) → ({𝑋} × {(𝐹‘𝑌)}) = {〈𝑋, (𝐹‘𝑌)〉}) |
| 25 | 23, 24 | mpan2 691 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝐴 → ({𝑋} × {(𝐹‘𝑌)}) = {〈𝑋, (𝐹‘𝑌)〉}) |
| 26 | 25 | 3ad2ant2 1135 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ({𝑋} × {(𝐹‘𝑌)}) = {〈𝑋, (𝐹‘𝑌)〉}) |
| 27 | 19, 22, 26 | 3eqtr3d 2785 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ {〈𝑋, 𝑌〉}) = {〈𝑋, (𝐹‘𝑌)〉}) |
| 28 | | fcoconst 7154 |
. . . . . . . . . . 11
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝐹 ∘ ({𝑌} × {𝑋})) = ({𝑌} × {(𝐹‘𝑋)})) |
| 29 | 28 | 3adant3 1133 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ ({𝑌} × {𝑋})) = ({𝑌} × {(𝐹‘𝑋)})) |
| 30 | | xpsng 7159 |
. . . . . . . . . . . . 13
⊢ ((𝑌 ∈ 𝐴 ∧ 𝑋 ∈ 𝐴) → ({𝑌} × {𝑋}) = {〈𝑌, 𝑋〉}) |
| 31 | 30 | coeq2d 5873 |
. . . . . . . . . . . 12
⊢ ((𝑌 ∈ 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝐹 ∘ ({𝑌} × {𝑋})) = (𝐹 ∘ {〈𝑌, 𝑋〉})) |
| 32 | 31 | ancoms 458 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ ({𝑌} × {𝑋})) = (𝐹 ∘ {〈𝑌, 𝑋〉})) |
| 33 | 32 | 3adant1 1131 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ ({𝑌} × {𝑋})) = (𝐹 ∘ {〈𝑌, 𝑋〉})) |
| 34 | | fvex 6919 |
. . . . . . . . . . . 12
⊢ (𝐹‘𝑋) ∈ V |
| 35 | | xpsng 7159 |
. . . . . . . . . . . 12
⊢ ((𝑌 ∈ 𝐴 ∧ (𝐹‘𝑋) ∈ V) → ({𝑌} × {(𝐹‘𝑋)}) = {〈𝑌, (𝐹‘𝑋)〉}) |
| 36 | 34, 35 | mpan2 691 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ 𝐴 → ({𝑌} × {(𝐹‘𝑋)}) = {〈𝑌, (𝐹‘𝑋)〉}) |
| 37 | 36 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ({𝑌} × {(𝐹‘𝑋)}) = {〈𝑌, (𝐹‘𝑋)〉}) |
| 38 | 29, 33, 37 | 3eqtr3d 2785 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ {〈𝑌, 𝑋〉}) = {〈𝑌, (𝐹‘𝑋)〉}) |
| 39 | 27, 38 | uneq12d 4169 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹 ∘ {〈𝑋, 𝑌〉}) ∪ (𝐹 ∘ {〈𝑌, 𝑋〉})) = ({〈𝑋, (𝐹‘𝑌)〉} ∪ {〈𝑌, (𝐹‘𝑋)〉})) |
| 40 | | df-pr 4629 |
. . . . . . . . . 10
⊢
{〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉} = ({〈𝑋, 𝑌〉} ∪ {〈𝑌, 𝑋〉}) |
| 41 | 40 | coeq2i 5871 |
. . . . . . . . 9
⊢ (𝐹 ∘ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}) = (𝐹 ∘ ({〈𝑋, 𝑌〉} ∪ {〈𝑌, 𝑋〉})) |
| 42 | | coundi 6267 |
. . . . . . . . 9
⊢ (𝐹 ∘ ({〈𝑋, 𝑌〉} ∪ {〈𝑌, 𝑋〉})) = ((𝐹 ∘ {〈𝑋, 𝑌〉}) ∪ (𝐹 ∘ {〈𝑌, 𝑋〉})) |
| 43 | 41, 42 | eqtri 2765 |
. . . . . . . 8
⊢ (𝐹 ∘ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}) = ((𝐹 ∘ {〈𝑋, 𝑌〉}) ∪ (𝐹 ∘ {〈𝑌, 𝑋〉})) |
| 44 | | df-pr 4629 |
. . . . . . . 8
⊢
{〈𝑋, (𝐹‘𝑌)〉, 〈𝑌, (𝐹‘𝑋)〉} = ({〈𝑋, (𝐹‘𝑌)〉} ∪ {〈𝑌, (𝐹‘𝑋)〉}) |
| 45 | 39, 43, 44 | 3eqtr4g 2802 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}) = {〈𝑋, (𝐹‘𝑌)〉, 〈𝑌, (𝐹‘𝑋)〉}) |
| 46 | 45 | uneq2d 4168 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹 ∘ ( I ↾ (𝐴 ∖ {𝑋, 𝑌}))) ∪ (𝐹 ∘ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉})) = ((𝐹 ∘ ( I ↾ (𝐴 ∖ {𝑋, 𝑌}))) ∪ {〈𝑋, (𝐹‘𝑌)〉, 〈𝑌, (𝐹‘𝑋)〉})) |
| 47 | 17, 46 | eqtrid 2789 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉})) = ((𝐹 ∘ ( I ↾ (𝐴 ∖ {𝑋, 𝑌}))) ∪ {〈𝑋, (𝐹‘𝑌)〉, 〈𝑌, (𝐹‘𝑋)〉})) |
| 48 | | coires1 6284 |
. . . . . 6
⊢ (𝐹 ∘ ( I ↾ (𝐴 ∖ {𝑋, 𝑌}))) = (𝐹 ↾ (𝐴 ∖ {𝑋, 𝑌})) |
| 49 | 48 | uneq1i 4164 |
. . . . 5
⊢ ((𝐹 ∘ ( I ↾ (𝐴 ∖ {𝑋, 𝑌}))) ∪ {〈𝑋, (𝐹‘𝑌)〉, 〈𝑌, (𝐹‘𝑋)〉}) = ((𝐹 ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, (𝐹‘𝑌)〉, 〈𝑌, (𝐹‘𝑋)〉}) |
| 50 | 47, 49 | eqtrdi 2793 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉})) = ((𝐹 ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, (𝐹‘𝑌)〉, 〈𝑌, (𝐹‘𝑋)〉})) |
| 51 | 16, 50 | syl3an1 1164 |
. . 3
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉})) = ((𝐹 ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, (𝐹‘𝑌)〉, 〈𝑌, (𝐹‘𝑋)〉})) |
| 52 | 51 | f1oeq1d 6843 |
. 2
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹 ∘ (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉})):𝐴–1-1-onto→𝐵 ↔ ((𝐹 ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, (𝐹‘𝑌)〉, 〈𝑌, (𝐹‘𝑋)〉}):𝐴–1-1-onto→𝐵)) |
| 53 | 15, 52 | mpbid 232 |
1
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹 ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, (𝐹‘𝑌)〉, 〈𝑌, (𝐹‘𝑋)〉}):𝐴–1-1-onto→𝐵) |