Step | Hyp | Ref
| Expression |
1 | | bren 8770 |
. . 3
⊢ (𝐴 ≈ suc 𝑀 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→suc
𝑀) |
2 | | 19.41v 1951 |
. . . . 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 304 |
. . . 4
⊢
(∃𝑓(𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) ↔ (∃𝑓 𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω)) |
7 | | sucidg 6357 |
. . . . . . . . 9
⊢ (𝑀 ∈ ω → 𝑀 ∈ suc 𝑀) |
8 | | f1ocnvdm 7185 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → (◡𝑓‘𝑀) ∈ 𝐴) |
9 | 8 | 3adant2 1131 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀) → (◡𝑓‘𝑀) ∈ 𝐴) |
10 | | f1ofvswap 7206 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ (◡𝑓‘𝑀) ∈ 𝐴) → ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, (𝑓‘(◡𝑓‘𝑀))⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩}):𝐴–1-1-onto→suc
𝑀) |
11 | 9, 10 | syld3an3 1409 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀) → ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, (𝑓‘(◡𝑓‘𝑀))⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩}):𝐴–1-1-onto→suc
𝑀) |
12 | | f1ocnvfv2 7177 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → (𝑓‘(◡𝑓‘𝑀)) = 𝑀) |
13 | 12 | opeq2d 4816 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → ⟨𝑋, (𝑓‘(◡𝑓‘𝑀))⟩ = ⟨𝑋, 𝑀⟩) |
14 | 13 | preq1d 4679 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → {⟨𝑋, (𝑓‘(◡𝑓‘𝑀))⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩} = {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩}) |
15 | 14 | uneq2d 4103 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, (𝑓‘(◡𝑓‘𝑀))⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩}) = ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩})) |
16 | 15 | f1oeq1d 6737 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → (((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, (𝑓‘(◡𝑓‘𝑀))⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩}):𝐴–1-1-onto→suc
𝑀 ↔ ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩}):𝐴–1-1-onto→suc
𝑀)) |
17 | 16 | 3adant2 1131 |
. . . . . . . . . . . 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 6744 |
. . . . . . . . . . 11
⊢ (((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩}):𝐴–1-1-onto→suc
𝑀 → Fun ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩})) |
20 | | opex 5388 |
. . . . . . . . . . . . . 14
⊢
⟨𝑋, 𝑀⟩ ∈ V |
21 | 20 | prid1 4702 |
. . . . . . . . . . . . 13
⊢
⟨𝑋, 𝑀⟩ ∈ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩} |
22 | | elun2 4117 |
. . . . . . . . . . . . 13
⊢
(⟨𝑋, 𝑀⟩ ∈ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩} → ⟨𝑋, 𝑀⟩ ∈ ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩})) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
⟨𝑋, 𝑀⟩ ∈ ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩}) |
24 | | funopfv 6849 |
. . . . . . . . . . . 12
⊢ (Fun
((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩}) → (⟨𝑋, 𝑀⟩ ∈ ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩}) → (((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩})‘𝑋) = 𝑀)) |
25 | 23, 24 | mpi 20 |
. . . . . . . . . . 11
⊢ (Fun
((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩}) → (((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩})‘𝑋) = 𝑀) |
26 | 18, 19, 25 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀) → (((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩})‘𝑋) = 𝑀) |
27 | | simp2 1137 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀) → 𝑋 ∈ 𝐴) |
28 | | f1ocnvfv 7178 |
. . . . . . . . . . 11
⊢ ((((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩}):𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴) → ((((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩})‘𝑋) = 𝑀 → (◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩})‘𝑀) = 𝑋)) |
29 | 18, 27, 28 | syl2anc 585 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀) → ((((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩})‘𝑋) = 𝑀 → (◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩})‘𝑀) = 𝑋)) |
30 | 26, 29 | mpd 15 |
. . . . . . . . 9
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀) → (◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩})‘𝑀) = 𝑋) |
31 | 7, 30 | syl3an3 1165 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) → (◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩})‘𝑀) = 𝑋) |
32 | 31 | sneqd 4577 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) → {(◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩})‘𝑀)} = {𝑋}) |
33 | 32 | difeq2d 4063 |
. . . . . 6
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) → (𝐴 ∖ {(◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩})‘𝑀)}) = (𝐴 ∖ {𝑋})) |
34 | | vex 3441 |
. . . . . . . . 9
⊢ 𝑓 ∈ V |
35 | 34 | resex 5947 |
. . . . . . . 8
⊢ (𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∈ V |
36 | | prex 5364 |
. . . . . . . 8
⊢
{⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩} ∈ V |
37 | 35, 36 | unex 7624 |
. . . . . . 7
⊢ ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩}) ∈ V |
38 | | simp3 1138 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) → 𝑀 ∈ ω) |
39 | 7, 18 | syl3an3 1165 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) → ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩}):𝐴–1-1-onto→suc
𝑀) |
40 | | dif1enlem 8977 |
. . . . . . 7
⊢ ((((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩}) ∈ V ∧ 𝑀 ∈ ω ∧ ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩}):𝐴–1-1-onto→suc
𝑀) → (𝐴 ∖ {(◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩})‘𝑀)}) ≈ 𝑀) |
41 | 37, 38, 39, 40 | mp3an2i 1466 |
. . . . . 6
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) → (𝐴 ∖ {(◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {⟨𝑋, 𝑀⟩, ⟨(◡𝑓‘𝑀), (𝑓‘𝑋)⟩})‘𝑀)}) ≈ 𝑀) |
42 | 33, 41 | eqbrtrrd 5105 |
. . . . 5
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) → (𝐴 ∖ {𝑋}) ≈ 𝑀) |
43 | 42 | exlimiv 1931 |
. . . 4
⊢
(∃𝑓(𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) → (𝐴 ∖ {𝑋}) ≈ 𝑀) |
44 | 6, 43 | sylbir 235 |
. . 3
⊢
((∃𝑓 𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) → (𝐴 ∖ {𝑋}) ≈ 𝑀) |
45 | 1, 44 | syl3an1b 1403 |
. 2
⊢ ((𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ ω) → (𝐴 ∖ {𝑋}) ≈ 𝑀) |
46 | 45 | 3comr 1125 |
1
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀) |