Proof of Theorem f1ofvswap
Step | Hyp | Ref
| Expression |
1 | | f1oi 6877 |
. . . . . 6
⊢ ( I
↾ (𝐴 ∖ {𝑋, 𝑌})):(𝐴 ∖ {𝑋, 𝑌})–1-1-onto→(𝐴 ∖ {𝑋, 𝑌}) |
2 | | f1oprswap 6883 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}:{𝑋, 𝑌}–1-1-onto→{𝑋, 𝑌}) |
3 | | disjdifr 4473 |
. . . . . . 7
⊢ ((𝐴 ∖ {𝑋, 𝑌}) ∩ {𝑋, 𝑌}) = ∅ |
4 | | f1oun 6858 |
. . . . . . 7
⊢ (((( I
↾ (𝐴 ∖ {𝑋, 𝑌})):(𝐴 ∖ {𝑋, 𝑌})–1-1-onto→(𝐴 ∖ {𝑋, 𝑌}) ∧ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}:{𝑋, 𝑌}–1-1-onto→{𝑋, 𝑌}) ∧ (((𝐴 ∖ {𝑋, 𝑌}) ∩ {𝑋, 𝑌}) = ∅ ∧ ((𝐴 ∖ {𝑋, 𝑌}) ∩ {𝑋, 𝑌}) = ∅)) → (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}):((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌})–1-1-onto→((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌})) |
5 | 3, 3, 4 | mpanr12 704 |
. . . . . 6
⊢ ((( I
↾ (𝐴 ∖ {𝑋, 𝑌})):(𝐴 ∖ {𝑋, 𝑌})–1-1-onto→(𝐴 ∖ {𝑋, 𝑌}) ∧ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}:{𝑋, 𝑌}–1-1-onto→{𝑋, 𝑌}) → (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}):((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌})–1-1-onto→((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌})) |
6 | 1, 2, 5 | sylancr 586 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}):((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌})–1-1-onto→((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌})) |
7 | | prssi 4825 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → {𝑋, 𝑌} ⊆ 𝐴) |
8 | | undifr 4483 |
. . . . . . 7
⊢ ({𝑋, 𝑌} ⊆ 𝐴 ↔ ((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌}) = 𝐴) |
9 | 7, 8 | sylib 217 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌}) = 𝐴) |
10 | | f1oeq23 6830 |
. . . . . 6
⊢ ((((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌}) = 𝐴 ∧ ((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌}) = 𝐴) → ((( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}):((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌})–1-1-onto→((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌}) ↔ (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}):𝐴–1-1-onto→𝐴)) |
11 | 9, 9, 10 | syl2anc 583 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}):((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌})–1-1-onto→((𝐴 ∖ {𝑋, 𝑌}) ∪ {𝑋, 𝑌}) ↔ (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}):𝐴–1-1-onto→𝐴)) |
12 | 6, 11 | mpbid 231 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}):𝐴–1-1-onto→𝐴) |
13 | | f1oco 6862 |
. . . 4
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}):𝐴–1-1-onto→𝐴) → (𝐹 ∘ (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉})):𝐴–1-1-onto→𝐵) |
14 | 12, 13 | sylan2 592 |
. . 3
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → (𝐹 ∘ (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉})):𝐴–1-1-onto→𝐵) |
15 | 14 | 3impb 1113 |
. 2
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉})):𝐴–1-1-onto→𝐵) |
16 | | f1ofn 6840 |
. . . 4
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴) |
17 | | coundi 6251 |
. . . . . 6
⊢ (𝐹 ∘ (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉})) = ((𝐹 ∘ ( I ↾ (𝐴 ∖ {𝑋, 𝑌}))) ∪ (𝐹 ∘ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉})) |
18 | | fcoconst 7143 |
. . . . . . . . . . 11
⊢ ((𝐹 Fn 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ ({𝑋} × {𝑌})) = ({𝑋} × {(𝐹‘𝑌)})) |
19 | 18 | 3adant2 1129 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ ({𝑋} × {𝑌})) = ({𝑋} × {(𝐹‘𝑌)})) |
20 | | xpsng 7148 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ({𝑋} × {𝑌}) = {〈𝑋, 𝑌〉}) |
21 | 20 | coeq2d 5865 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ ({𝑋} × {𝑌})) = (𝐹 ∘ {〈𝑋, 𝑌〉})) |
22 | 21 | 3adant1 1128 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ ({𝑋} × {𝑌})) = (𝐹 ∘ {〈𝑋, 𝑌〉})) |
23 | | fvex 6910 |
. . . . . . . . . . . 12
⊢ (𝐹‘𝑌) ∈ V |
24 | | xpsng 7148 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ 𝐴 ∧ (𝐹‘𝑌) ∈ V) → ({𝑋} × {(𝐹‘𝑌)}) = {〈𝑋, (𝐹‘𝑌)〉}) |
25 | 23, 24 | mpan2 690 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ 𝐴 → ({𝑋} × {(𝐹‘𝑌)}) = {〈𝑋, (𝐹‘𝑌)〉}) |
26 | 25 | 3ad2ant2 1132 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ({𝑋} × {(𝐹‘𝑌)}) = {〈𝑋, (𝐹‘𝑌)〉}) |
27 | 19, 22, 26 | 3eqtr3d 2776 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ {〈𝑋, 𝑌〉}) = {〈𝑋, (𝐹‘𝑌)〉}) |
28 | | fcoconst 7143 |
. . . . . . . . . . 11
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝐹 ∘ ({𝑌} × {𝑋})) = ({𝑌} × {(𝐹‘𝑋)})) |
29 | 28 | 3adant3 1130 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ ({𝑌} × {𝑋})) = ({𝑌} × {(𝐹‘𝑋)})) |
30 | | xpsng 7148 |
. . . . . . . . . . . . 13
⊢ ((𝑌 ∈ 𝐴 ∧ 𝑋 ∈ 𝐴) → ({𝑌} × {𝑋}) = {〈𝑌, 𝑋〉}) |
31 | 30 | coeq2d 5865 |
. . . . . . . . . . . 12
⊢ ((𝑌 ∈ 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝐹 ∘ ({𝑌} × {𝑋})) = (𝐹 ∘ {〈𝑌, 𝑋〉})) |
32 | 31 | ancoms 458 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ ({𝑌} × {𝑋})) = (𝐹 ∘ {〈𝑌, 𝑋〉})) |
33 | 32 | 3adant1 1128 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ ({𝑌} × {𝑋})) = (𝐹 ∘ {〈𝑌, 𝑋〉})) |
34 | | fvex 6910 |
. . . . . . . . . . . 12
⊢ (𝐹‘𝑋) ∈ V |
35 | | xpsng 7148 |
. . . . . . . . . . . 12
⊢ ((𝑌 ∈ 𝐴 ∧ (𝐹‘𝑋) ∈ V) → ({𝑌} × {(𝐹‘𝑋)}) = {〈𝑌, (𝐹‘𝑋)〉}) |
36 | 34, 35 | mpan2 690 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ 𝐴 → ({𝑌} × {(𝐹‘𝑋)}) = {〈𝑌, (𝐹‘𝑋)〉}) |
37 | 36 | 3ad2ant3 1133 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ({𝑌} × {(𝐹‘𝑋)}) = {〈𝑌, (𝐹‘𝑋)〉}) |
38 | 29, 33, 37 | 3eqtr3d 2776 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ {〈𝑌, 𝑋〉}) = {〈𝑌, (𝐹‘𝑋)〉}) |
39 | 27, 38 | uneq12d 4163 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹 ∘ {〈𝑋, 𝑌〉}) ∪ (𝐹 ∘ {〈𝑌, 𝑋〉})) = ({〈𝑋, (𝐹‘𝑌)〉} ∪ {〈𝑌, (𝐹‘𝑋)〉})) |
40 | | df-pr 4632 |
. . . . . . . . . 10
⊢
{〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉} = ({〈𝑋, 𝑌〉} ∪ {〈𝑌, 𝑋〉}) |
41 | 40 | coeq2i 5863 |
. . . . . . . . 9
⊢ (𝐹 ∘ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}) = (𝐹 ∘ ({〈𝑋, 𝑌〉} ∪ {〈𝑌, 𝑋〉})) |
42 | | coundi 6251 |
. . . . . . . . 9
⊢ (𝐹 ∘ ({〈𝑋, 𝑌〉} ∪ {〈𝑌, 𝑋〉})) = ((𝐹 ∘ {〈𝑋, 𝑌〉}) ∪ (𝐹 ∘ {〈𝑌, 𝑋〉})) |
43 | 41, 42 | eqtri 2756 |
. . . . . . . 8
⊢ (𝐹 ∘ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}) = ((𝐹 ∘ {〈𝑋, 𝑌〉}) ∪ (𝐹 ∘ {〈𝑌, 𝑋〉})) |
44 | | df-pr 4632 |
. . . . . . . 8
⊢
{〈𝑋, (𝐹‘𝑌)〉, 〈𝑌, (𝐹‘𝑋)〉} = ({〈𝑋, (𝐹‘𝑌)〉} ∪ {〈𝑌, (𝐹‘𝑋)〉}) |
45 | 39, 43, 44 | 3eqtr4g 2793 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉}) = {〈𝑋, (𝐹‘𝑌)〉, 〈𝑌, (𝐹‘𝑋)〉}) |
46 | 45 | uneq2d 4162 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹 ∘ ( I ↾ (𝐴 ∖ {𝑋, 𝑌}))) ∪ (𝐹 ∘ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉})) = ((𝐹 ∘ ( I ↾ (𝐴 ∖ {𝑋, 𝑌}))) ∪ {〈𝑋, (𝐹‘𝑌)〉, 〈𝑌, (𝐹‘𝑋)〉})) |
47 | 17, 46 | eqtrid 2780 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉})) = ((𝐹 ∘ ( I ↾ (𝐴 ∖ {𝑋, 𝑌}))) ∪ {〈𝑋, (𝐹‘𝑌)〉, 〈𝑌, (𝐹‘𝑋)〉})) |
48 | | coires1 6268 |
. . . . . 6
⊢ (𝐹 ∘ ( I ↾ (𝐴 ∖ {𝑋, 𝑌}))) = (𝐹 ↾ (𝐴 ∖ {𝑋, 𝑌})) |
49 | 48 | uneq1i 4158 |
. . . . 5
⊢ ((𝐹 ∘ ( I ↾ (𝐴 ∖ {𝑋, 𝑌}))) ∪ {〈𝑋, (𝐹‘𝑌)〉, 〈𝑌, (𝐹‘𝑋)〉}) = ((𝐹 ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, (𝐹‘𝑌)〉, 〈𝑌, (𝐹‘𝑋)〉}) |
50 | 47, 49 | eqtrdi 2784 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉})) = ((𝐹 ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, (𝐹‘𝑌)〉, 〈𝑌, (𝐹‘𝑋)〉})) |
51 | 16, 50 | syl3an1 1161 |
. . 3
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝐹 ∘ (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉})) = ((𝐹 ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, (𝐹‘𝑌)〉, 〈𝑌, (𝐹‘𝑋)〉})) |
52 | 51 | f1oeq1d 6834 |
. 2
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹 ∘ (( I ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, 𝑌〉, 〈𝑌, 𝑋〉})):𝐴–1-1-onto→𝐵 ↔ ((𝐹 ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, (𝐹‘𝑌)〉, 〈𝑌, (𝐹‘𝑋)〉}):𝐴–1-1-onto→𝐵)) |
53 | 15, 52 | mpbid 231 |
1
⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹 ↾ (𝐴 ∖ {𝑋, 𝑌})) ∪ {〈𝑋, (𝐹‘𝑌)〉, 〈𝑌, (𝐹‘𝑋)〉}):𝐴–1-1-onto→𝐵) |