| Step | Hyp | Ref
| Expression |
| 1 | | simp1 1137 |
. . 3
⊢ ((𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On) → 𝐴 ≈ suc 𝑀) |
| 2 | | encv 8993 |
. . . . 5
⊢ (𝐴 ≈ suc 𝑀 → (𝐴 ∈ V ∧ suc 𝑀 ∈ V)) |
| 3 | 2 | simpld 494 |
. . . 4
⊢ (𝐴 ≈ suc 𝑀 → 𝐴 ∈ V) |
| 4 | 3 | 3anim1i 1153 |
. . 3
⊢ ((𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On) → (𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On)) |
| 5 | | bren 8995 |
. . . 4
⊢ (𝐴 ≈ suc 𝑀 ↔ ∃𝑓 𝑓:𝐴–1-1-onto→suc
𝑀) |
| 6 | | sucidg 6465 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ On → 𝑀 ∈ suc 𝑀) |
| 7 | | f1ocnvdm 7305 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → (◡𝑓‘𝑀) ∈ 𝐴) |
| 8 | 7 | 3adant2 1132 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀) → (◡𝑓‘𝑀) ∈ 𝐴) |
| 9 | | f1ofvswap 7326 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ (◡𝑓‘𝑀) ∈ 𝐴) → ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, (𝑓‘(◡𝑓‘𝑀))〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀) |
| 10 | 8, 9 | syld3an3 1411 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀) → ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, (𝑓‘(◡𝑓‘𝑀))〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀) |
| 11 | | f1ocnvfv2 7297 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → (𝑓‘(◡𝑓‘𝑀)) = 𝑀) |
| 12 | 11 | opeq2d 4880 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → 〈𝑋, (𝑓‘(◡𝑓‘𝑀))〉 = 〈𝑋, 𝑀〉) |
| 13 | 12 | preq1d 4739 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → {〈𝑋, (𝑓‘(◡𝑓‘𝑀))〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉} = {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}) |
| 14 | 13 | uneq2d 4168 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, (𝑓‘(◡𝑓‘𝑀))〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}) = ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})) |
| 15 | 14 | f1oeq1d 6843 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑀 ∈ suc 𝑀) → (((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, (𝑓‘(◡𝑓‘𝑀))〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀 ↔ ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀)) |
| 16 | 15 | 3adant2 1132 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀) → (((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, (𝑓‘(◡𝑓‘𝑀))〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀 ↔ ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀)) |
| 17 | 10, 16 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ suc 𝑀) → ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀) |
| 18 | 6, 17 | syl3an3 1166 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On) → ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀) |
| 19 | 18 | 3adant3r1 1183 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ (𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On)) → ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀) |
| 20 | | f1ofun 6850 |
. . . . . . . . . . 11
⊢ (((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀 → Fun ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})) |
| 21 | | opex 5469 |
. . . . . . . . . . . . . 14
⊢
〈𝑋, 𝑀〉 ∈ V |
| 22 | 21 | prid1 4762 |
. . . . . . . . . . . . 13
⊢
〈𝑋, 𝑀〉 ∈ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉} |
| 23 | | elun2 4183 |
. . . . . . . . . . . . 13
⊢
(〈𝑋, 𝑀〉 ∈ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉} → 〈𝑋, 𝑀〉 ∈ ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})) |
| 24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
〈𝑋, 𝑀〉 ∈ ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}) |
| 25 | | funopfv 6958 |
. . . . . . . . . . . 12
⊢ (Fun
((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}) → (〈𝑋, 𝑀〉 ∈ ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}) → (((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑋) = 𝑀)) |
| 26 | 24, 25 | mpi 20 |
. . . . . . . . . . 11
⊢ (Fun
((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}) → (((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑋) = 𝑀) |
| 27 | 19, 20, 26 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ (𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On)) → (((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑋) = 𝑀) |
| 28 | | simpr2 1196 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ (𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On)) → 𝑋 ∈ 𝐴) |
| 29 | | f1ocnvfv 7298 |
. . . . . . . . . . 11
⊢ ((((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴) → ((((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑋) = 𝑀 → (◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑀) = 𝑋)) |
| 30 | 19, 28, 29 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ (𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On)) → ((((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑋) = 𝑀 → (◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑀) = 𝑋)) |
| 31 | 27, 30 | mpd 15 |
. . . . . . . . 9
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ (𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On)) → (◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑀) = 𝑋) |
| 32 | 31 | sneqd 4638 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ (𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On)) → {(◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑀)} = {𝑋}) |
| 33 | 32 | difeq2d 4126 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ (𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On)) → (𝐴 ∖ {(◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑀)}) = (𝐴 ∖ {𝑋})) |
| 34 | | simpr1 1195 |
. . . . . . . . 9
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ (𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On)) → 𝐴 ∈ V) |
| 35 | | 3simpc 1151 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On) → (𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On)) |
| 36 | 35 | anim2i 617 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ (𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On)) → (𝑓:𝐴–1-1-onto→suc
𝑀 ∧ (𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On))) |
| 37 | | 3anass 1095 |
. . . . . . . . . 10
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On) ↔ (𝑓:𝐴–1-1-onto→suc
𝑀 ∧ (𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On))) |
| 38 | 36, 37 | sylibr 234 |
. . . . . . . . 9
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ (𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On)) → (𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On)) |
| 39 | 34, 38 | jca 511 |
. . . . . . . 8
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ (𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On)) → (𝐴 ∈ V ∧ (𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On))) |
| 40 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ (𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On)) → 𝐴 ∈ V) |
| 41 | | simpr3 1197 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ (𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On)) → 𝑀 ∈ On) |
| 42 | 40, 41 | jca 511 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ (𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On)) → (𝐴 ∈ V ∧ 𝑀 ∈ On)) |
| 43 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧ (𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On)) → (𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On)) |
| 44 | 42, 43 | jca 511 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ (𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On)) → ((𝐴 ∈ V ∧ 𝑀 ∈ On) ∧ (𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On))) |
| 45 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑓 ∈ V |
| 46 | 45 | resex 6047 |
. . . . . . . . . . 11
⊢ (𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∈ V |
| 47 | | prex 5437 |
. . . . . . . . . . 11
⊢
{〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉} ∈ V |
| 48 | 46, 47 | unex 7764 |
. . . . . . . . . 10
⊢ ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}) ∈ V |
| 49 | | dif1enlem 9196 |
. . . . . . . . . 10
⊢
(((((𝑓 ↾
(𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}) ∈ V ∧ 𝐴 ∈ V ∧ 𝑀 ∈ On) ∧ ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀) → (𝐴 ∖ {(◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑀)}) ≈ 𝑀) |
| 50 | 48, 49 | mp3anl1 1457 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ 𝑀 ∈ On) ∧ ((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉}):𝐴–1-1-onto→suc
𝑀) → (𝐴 ∖ {(◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑀)}) ≈ 𝑀) |
| 51 | 18, 50 | sylan2 593 |
. . . . . . . 8
⊢ (((𝐴 ∈ V ∧ 𝑀 ∈ On) ∧ (𝑓:𝐴–1-1-onto→suc
𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On)) → (𝐴 ∖ {(◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑀)}) ≈ 𝑀) |
| 52 | 39, 44, 51 | 3syl 18 |
. . . . . . 7
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ (𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On)) → (𝐴 ∖ {(◡((𝑓 ↾ (𝐴 ∖ {𝑋, (◡𝑓‘𝑀)})) ∪ {〈𝑋, 𝑀〉, 〈(◡𝑓‘𝑀), (𝑓‘𝑋)〉})‘𝑀)}) ≈ 𝑀) |
| 53 | 33, 52 | eqbrtrrd 5167 |
. . . . . 6
⊢ ((𝑓:𝐴–1-1-onto→suc
𝑀 ∧ (𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On)) → (𝐴 ∖ {𝑋}) ≈ 𝑀) |
| 54 | 53 | ex 412 |
. . . . 5
⊢ (𝑓:𝐴–1-1-onto→suc
𝑀 → ((𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On) → (𝐴 ∖ {𝑋}) ≈ 𝑀)) |
| 55 | 54 | exlimiv 1930 |
. . . 4
⊢
(∃𝑓 𝑓:𝐴–1-1-onto→suc
𝑀 → ((𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On) → (𝐴 ∖ {𝑋}) ≈ 𝑀)) |
| 56 | 5, 55 | sylbi 217 |
. . 3
⊢ (𝐴 ≈ suc 𝑀 → ((𝐴 ∈ V ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On) → (𝐴 ∖ {𝑋}) ≈ 𝑀)) |
| 57 | 1, 4, 56 | sylc 65 |
. 2
⊢ ((𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ∧ 𝑀 ∈ On) → (𝐴 ∖ {𝑋}) ≈ 𝑀) |
| 58 | 57 | 3comr 1126 |
1
⊢ ((𝑀 ∈ On ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀) |