Step | Hyp | Ref
| Expression |
1 | | peano2 7086 |
. . . . 5
⊢ (𝑀 ∈ ω → suc 𝑀 ∈
ω) |
2 | | breq2 4657 |
. . . . . . 7
⊢ (𝑥 = suc 𝑀 → (𝐴 ≈ 𝑥 ↔ 𝐴 ≈ suc 𝑀)) |
3 | 2 | rspcev 3309 |
. . . . . 6
⊢ ((suc
𝑀 ∈ ω ∧
𝐴 ≈ suc 𝑀) → ∃𝑥 ∈ ω 𝐴 ≈ 𝑥) |
4 | | isfi 7979 |
. . . . . 6
⊢ (𝐴 ∈ Fin ↔ ∃𝑥 ∈ ω 𝐴 ≈ 𝑥) |
5 | 3, 4 | sylibr 224 |
. . . . 5
⊢ ((suc
𝑀 ∈ ω ∧
𝐴 ≈ suc 𝑀) → 𝐴 ∈ Fin) |
6 | 1, 5 | sylan 488 |
. . . 4
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀) → 𝐴 ∈ Fin) |
7 | | diffi 8192 |
. . . . 5
⊢ (𝐴 ∈ Fin → (𝐴 ∖ {𝑋}) ∈ Fin) |
8 | | isfi 7979 |
. . . . 5
⊢ ((𝐴 ∖ {𝑋}) ∈ Fin ↔ ∃𝑥 ∈ ω (𝐴 ∖ {𝑋}) ≈ 𝑥) |
9 | 7, 8 | sylib 208 |
. . . 4
⊢ (𝐴 ∈ Fin → ∃𝑥 ∈ ω (𝐴 ∖ {𝑋}) ≈ 𝑥) |
10 | 6, 9 | syl 17 |
. . 3
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀) → ∃𝑥 ∈ ω (𝐴 ∖ {𝑋}) ≈ 𝑥) |
11 | 10 | 3adant3 1081 |
. 2
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → ∃𝑥 ∈ ω (𝐴 ∖ {𝑋}) ≈ 𝑥) |
12 | | vex 3203 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
13 | | en2sn 8037 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑥 ∈ V) → {𝑋} ≈ {𝑥}) |
14 | 12, 13 | mpan2 707 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐴 → {𝑋} ≈ {𝑥}) |
15 | | nnord 7073 |
. . . . . . . 8
⊢ (𝑥 ∈ ω → Ord 𝑥) |
16 | | orddisj 5762 |
. . . . . . . 8
⊢ (Ord
𝑥 → (𝑥 ∩ {𝑥}) = ∅) |
17 | 15, 16 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ ω → (𝑥 ∩ {𝑥}) = ∅) |
18 | | incom 3805 |
. . . . . . . . . 10
⊢ ((𝐴 ∖ {𝑋}) ∩ {𝑋}) = ({𝑋} ∩ (𝐴 ∖ {𝑋})) |
19 | | disjdif 4040 |
. . . . . . . . . 10
⊢ ({𝑋} ∩ (𝐴 ∖ {𝑋})) = ∅ |
20 | 18, 19 | eqtri 2644 |
. . . . . . . . 9
⊢ ((𝐴 ∖ {𝑋}) ∩ {𝑋}) = ∅ |
21 | | unen 8040 |
. . . . . . . . . 10
⊢ ((((𝐴 ∖ {𝑋}) ≈ 𝑥 ∧ {𝑋} ≈ {𝑥}) ∧ (((𝐴 ∖ {𝑋}) ∩ {𝑋}) = ∅ ∧ (𝑥 ∩ {𝑥}) = ∅)) → ((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑥 ∪ {𝑥})) |
22 | 21 | an4s 869 |
. . . . . . . . 9
⊢ ((((𝐴 ∖ {𝑋}) ≈ 𝑥 ∧ ((𝐴 ∖ {𝑋}) ∩ {𝑋}) = ∅) ∧ ({𝑋} ≈ {𝑥} ∧ (𝑥 ∩ {𝑥}) = ∅)) → ((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑥 ∪ {𝑥})) |
23 | 20, 22 | mpanl2 717 |
. . . . . . . 8
⊢ (((𝐴 ∖ {𝑋}) ≈ 𝑥 ∧ ({𝑋} ≈ {𝑥} ∧ (𝑥 ∩ {𝑥}) = ∅)) → ((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑥 ∪ {𝑥})) |
24 | 23 | expcom 451 |
. . . . . . 7
⊢ (({𝑋} ≈ {𝑥} ∧ (𝑥 ∩ {𝑥}) = ∅) → ((𝐴 ∖ {𝑋}) ≈ 𝑥 → ((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑥 ∪ {𝑥}))) |
25 | 14, 17, 24 | syl2an 494 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑥 ∈ ω) → ((𝐴 ∖ {𝑋}) ≈ 𝑥 → ((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑥 ∪ {𝑥}))) |
26 | 25 | 3ad2antl3 1225 |
. . . . 5
⊢ (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) ∧ 𝑥 ∈ ω) → ((𝐴 ∖ {𝑋}) ≈ 𝑥 → ((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑥 ∪ {𝑥}))) |
27 | | difsnid 4341 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝐴 → ((𝐴 ∖ {𝑋}) ∪ {𝑋}) = 𝐴) |
28 | | df-suc 5729 |
. . . . . . . . . . 11
⊢ suc 𝑥 = (𝑥 ∪ {𝑥}) |
29 | 28 | eqcomi 2631 |
. . . . . . . . . 10
⊢ (𝑥 ∪ {𝑥}) = suc 𝑥 |
30 | 29 | a1i 11 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝐴 → (𝑥 ∪ {𝑥}) = suc 𝑥) |
31 | 27, 30 | breq12d 4666 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐴 → (((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑥 ∪ {𝑥}) ↔ 𝐴 ≈ suc 𝑥)) |
32 | 31 | 3ad2ant3 1084 |
. . . . . . 7
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑥 ∪ {𝑥}) ↔ 𝐴 ≈ suc 𝑥)) |
33 | 32 | adantr 481 |
. . . . . 6
⊢ (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) ∧ 𝑥 ∈ ω) → (((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑥 ∪ {𝑥}) ↔ 𝐴 ≈ suc 𝑥)) |
34 | | ensym 8005 |
. . . . . . . . . . 11
⊢ (𝐴 ≈ suc 𝑀 → suc 𝑀 ≈ 𝐴) |
35 | | entr 8008 |
. . . . . . . . . . . . 13
⊢ ((suc
𝑀 ≈ 𝐴 ∧ 𝐴 ≈ suc 𝑥) → suc 𝑀 ≈ suc 𝑥) |
36 | | peano2 7086 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ω → suc 𝑥 ∈
ω) |
37 | | nneneq 8143 |
. . . . . . . . . . . . . 14
⊢ ((suc
𝑀 ∈ ω ∧ suc
𝑥 ∈ ω) →
(suc 𝑀 ≈ suc 𝑥 ↔ suc 𝑀 = suc 𝑥)) |
38 | 36, 37 | sylan2 491 |
. . . . . . . . . . . . 13
⊢ ((suc
𝑀 ∈ ω ∧
𝑥 ∈ ω) →
(suc 𝑀 ≈ suc 𝑥 ↔ suc 𝑀 = suc 𝑥)) |
39 | 35, 38 | syl5ib 234 |
. . . . . . . . . . . 12
⊢ ((suc
𝑀 ∈ ω ∧
𝑥 ∈ ω) →
((suc 𝑀 ≈ 𝐴 ∧ 𝐴 ≈ suc 𝑥) → suc 𝑀 = suc 𝑥)) |
40 | 39 | expd 452 |
. . . . . . . . . . 11
⊢ ((suc
𝑀 ∈ ω ∧
𝑥 ∈ ω) →
(suc 𝑀 ≈ 𝐴 → (𝐴 ≈ suc 𝑥 → suc 𝑀 = suc 𝑥))) |
41 | 34, 40 | syl5 34 |
. . . . . . . . . 10
⊢ ((suc
𝑀 ∈ ω ∧
𝑥 ∈ ω) →
(𝐴 ≈ suc 𝑀 → (𝐴 ≈ suc 𝑥 → suc 𝑀 = suc 𝑥))) |
42 | 1, 41 | sylan 488 |
. . . . . . . . 9
⊢ ((𝑀 ∈ ω ∧ 𝑥 ∈ ω) → (𝐴 ≈ suc 𝑀 → (𝐴 ≈ suc 𝑥 → suc 𝑀 = suc 𝑥))) |
43 | 42 | imp 445 |
. . . . . . . 8
⊢ (((𝑀 ∈ ω ∧ 𝑥 ∈ ω) ∧ 𝐴 ≈ suc 𝑀) → (𝐴 ≈ suc 𝑥 → suc 𝑀 = suc 𝑥)) |
44 | 43 | an32s 846 |
. . . . . . 7
⊢ (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀) ∧ 𝑥 ∈ ω) → (𝐴 ≈ suc 𝑥 → suc 𝑀 = suc 𝑥)) |
45 | 44 | 3adantl3 1219 |
. . . . . 6
⊢ (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) ∧ 𝑥 ∈ ω) → (𝐴 ≈ suc 𝑥 → suc 𝑀 = suc 𝑥)) |
46 | 33, 45 | sylbid 230 |
. . . . 5
⊢ (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) ∧ 𝑥 ∈ ω) → (((𝐴 ∖ {𝑋}) ∪ {𝑋}) ≈ (𝑥 ∪ {𝑥}) → suc 𝑀 = suc 𝑥)) |
47 | | peano4 7088 |
. . . . . . 7
⊢ ((𝑀 ∈ ω ∧ 𝑥 ∈ ω) → (suc
𝑀 = suc 𝑥 ↔ 𝑀 = 𝑥)) |
48 | 47 | biimpd 219 |
. . . . . 6
⊢ ((𝑀 ∈ ω ∧ 𝑥 ∈ ω) → (suc
𝑀 = suc 𝑥 → 𝑀 = 𝑥)) |
49 | 48 | 3ad2antl1 1223 |
. . . . 5
⊢ (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) ∧ 𝑥 ∈ ω) → (suc 𝑀 = suc 𝑥 → 𝑀 = 𝑥)) |
50 | 26, 46, 49 | 3syld 60 |
. . . 4
⊢ (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) ∧ 𝑥 ∈ ω) → ((𝐴 ∖ {𝑋}) ≈ 𝑥 → 𝑀 = 𝑥)) |
51 | | breq2 4657 |
. . . . 5
⊢ (𝑀 = 𝑥 → ((𝐴 ∖ {𝑋}) ≈ 𝑀 ↔ (𝐴 ∖ {𝑋}) ≈ 𝑥)) |
52 | 51 | biimprcd 240 |
. . . 4
⊢ ((𝐴 ∖ {𝑋}) ≈ 𝑥 → (𝑀 = 𝑥 → (𝐴 ∖ {𝑋}) ≈ 𝑀)) |
53 | 50, 52 | sylcom 30 |
. . 3
⊢ (((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) ∧ 𝑥 ∈ ω) → ((𝐴 ∖ {𝑋}) ≈ 𝑥 → (𝐴 ∖ {𝑋}) ≈ 𝑀)) |
54 | 53 | rexlimdva 3031 |
. 2
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (∃𝑥 ∈ ω (𝐴 ∖ {𝑋}) ≈ 𝑥 → (𝐴 ∖ {𝑋}) ≈ 𝑀)) |
55 | 11, 54 | mpd 15 |
1
⊢ ((𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴) → (𝐴 ∖ {𝑋}) ≈ 𝑀) |