| Step | Hyp | Ref
| Expression |
| 1 | | bren 8995 |
. . 3
⊢ (𝐴 ≈ suc 𝑀 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→suc
𝑀) |
| 2 | | 19.41v 1949 |
. . . . 5
⊢
(∃𝑓(𝑓:𝐴–1-1-onto→suc
𝑀 ∧ (𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω)) ↔ (∃𝑓 𝑓:𝐴–1-1-onto→suc
𝑀 ∧ (𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω))) |
| 3 | | 3anass 1095 |
. . . . . 6
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) ↔ (𝑓:𝐴–1-1-onto→suc
𝑀 ∧ (𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω))) |
| 4 | 3 | exbii 1848 |
. . . . 5
⊢
(∃𝑓(𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) ↔ ∃𝑓(𝑓:𝐴–1-1-onto→suc
𝑀 ∧ (𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω))) |
| 5 | | 3anass 1095 |
. . . . 5
⊢
((∃𝑓 𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) ↔ (∃𝑓 𝑓:𝐴–1-1-onto→suc
𝑀 ∧ (𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω))) |
| 6 | 2, 4, 5 | 3bitr4i 303 |
. . . 4
⊢
(∃𝑓(𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) ↔ (∃𝑓 𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω)) |
| 7 | | sucidg 6465 |
. . . . . . . . 9
⊢ (𝑀 ∈ ω → 𝑀 ∈ suc 𝑀) |
| 8 | | f1ocnvdm 7305 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → (◡𝑓‘𝑀) ∈ 𝐴) |
| 9 | 8 | 3adant2 1132 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀) → (◡𝑓‘𝑀) ∈ 𝐴) |
| 10 | | f1ofvswap 7326 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ (◡𝑓‘𝑀) ∈ 𝐴) → ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, (𝑓‘(◡𝑓‘𝑀))〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀) |
| 11 | 9, 10 | syld3an3 1411 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀) → ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, (𝑓‘(◡𝑓‘𝑀))〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀) |
| 12 | | f1ocnvfv2 7297 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → (𝑓‘(◡𝑓‘𝑀)) = 𝑀) |
| 13 | 12 | opeq2d 4880 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → 〈𝑋, (𝑓‘(◡𝑓‘𝑀))〉 = 〈𝑋, 𝑀〉) |
| 14 | 13 | preq1d 4739 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → {〈𝑋, (𝑓‘(◡𝑓‘𝑀))〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉} = {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}) |
| 15 | 14 | uneq2d 4168 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, (𝑓‘(◡𝑓‘𝑀))〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}) = ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})) |
| 16 | 15 | f1oeq1d 6843 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → (((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, (𝑓‘(◡𝑓‘𝑀))〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀 ↔ ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀)) |
| 17 | 16 | 3adant2 1132 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀) → (((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, (𝑓‘(◡𝑓‘𝑀))〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀 ↔ ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀)) |
| 18 | 11, 17 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀) → ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀) |
| 19 | | f1ofun 6850 |
. . . . . . . . . . 11
⊢ (((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀 → Fun ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})) |
| 20 | | opex 5469 |
. . . . . . . . . . . . . 14
⊢
〈𝑋, 𝑀〉 ∈ V |
| 21 | 20 | prid1 4762 |
. . . . . . . . . . . . 13
⊢
〈𝑋, 𝑀〉 ∈ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉} |
| 22 | | elun2 4183 |
. . . . . . . . . . . . 13
⊢
(〈𝑋, 𝑀〉 ∈ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉} → 〈𝑋, 𝑀〉 ∈ ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})) |
| 23 | 21, 22 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
〈𝑋, 𝑀〉 ∈ ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}) |
| 24 | | funopfv 6958 |
. . . . . . . . . . . 12
⊢ (Fun
((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}) → (〈𝑋, 𝑀〉 ∈ ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}) → (((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑋) = 𝑀)) |
| 25 | 23, 24 | mpi 20 |
. . . . . . . . . . 11
⊢ (Fun
((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}) → (((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑋) = 𝑀) |
| 26 | 18, 19, 25 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀) → (((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑋) = 𝑀) |
| 27 | | simp2 1138 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀) → 𝑋 ∈ 𝐴) |
| 28 | | f1ocnvfv 7298 |
. . . . . . . . . . 11
⊢ ((((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴) → ((((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑋) = 𝑀 → (◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑀) = 𝑋)) |
| 29 | 18, 27, 28 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀) → ((((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑋) = 𝑀 → (◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑀) = 𝑋)) |
| 30 | 26, 29 | mpd 15 |
. . . . . . . . 9
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀) → (◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑀) = 𝑋) |
| 31 | 7, 30 | syl3an3 1166 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) → (◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑀) = 𝑋) |
| 32 | 31 | sneqd 4638 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) → {(◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑀)} = {𝑋}) |
| 33 | 32 | difeq2d 4126 |
. . . . . 6
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) → (𝐴 ∖ {(◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑀)}) = (𝐴 ∖ {𝑋})) |
| 34 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑓 ∈ V |
| 35 | 34 | resex 6047 |
. . . . . . . 8
⊢ (𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∈ V |
| 36 | | prex 5437 |
. . . . . . . 8
⊢
{〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉} ∈ V |
| 37 | 35, 36 | unex 7764 |
. . . . . . 7
⊢ ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}) ∈ V |
| 38 | | simp3 1139 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) → 𝑀 ∈ ω) |
| 39 | 7, 18 | syl3an3 1166 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) → ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀) |
| 40 | | dif1enlemOLD 9197 |
. . . . . . 7
⊢ ((((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}) ∈ V ∧ 𝑀 ∈ ω ∧ ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀) → (𝐴 ∖ {(◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑀)}) ≈ 𝑀) |
| 41 | 37, 38, 39, 40 | mp3an2i 1468 |
. . . . . 6
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) → (𝐴 ∖ {(◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑀)}) ≈ 𝑀) |
| 42 | 33, 41 | eqbrtrrd 5167 |
. . . . 5
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) → (𝐴 ∖ {𝑋}) ≈ 𝑀) |
| 43 | 42 | exlimiv 1930 |
. . . 4
⊢
(∃𝑓(𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) → (𝐴 ∖ {𝑋}) ≈ 𝑀) |
| 44 | 6, 43 | sylbir 235 |
. . 3
⊢
((∃𝑓 𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) → (𝐴 ∖ {𝑋}) ≈ 𝑀) |
| 45 | 1, 44 | syl3an1b 1405 |
. 2
⊢ ((𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) → (𝐴 ∖ {𝑋}) ≈ 𝑀) |
| 46 | 45 | 3comr 1126 |
1
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀) |