Step | Hyp | Ref
| Expression |
1 | | zfz1isolem1.xz |
. . . . . 6
⊢ (𝜑 → 𝑋 ⊆ ℤ) |
2 | 1 | ssdifssd 3265 |
. . . . 5
⊢ (𝜑 → (𝑋 ∖ {𝑀}) ⊆ ℤ) |
3 | | zfz1isolem1.xf |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ Fin) |
4 | | zfz1isolem1.mx |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ 𝑋) |
5 | | diffisn 6871 |
. . . . . 6
⊢ ((𝑋 ∈ Fin ∧ 𝑀 ∈ 𝑋) → (𝑋 ∖ {𝑀}) ∈ Fin) |
6 | 3, 4, 5 | syl2anc 409 |
. . . . 5
⊢ (𝜑 → (𝑋 ∖ {𝑀}) ∈ Fin) |
7 | | zfz1isolem1.k |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ ω) |
8 | | zfz1isolem1.xs |
. . . . . 6
⊢ (𝜑 → 𝑋 ≈ suc 𝐾) |
9 | | dif1en 6857 |
. . . . . 6
⊢ ((𝐾 ∈ ω ∧ 𝑋 ≈ suc 𝐾 ∧ 𝑀 ∈ 𝑋) → (𝑋 ∖ {𝑀}) ≈ 𝐾) |
10 | 7, 8, 4, 9 | syl3anc 1233 |
. . . . 5
⊢ (𝜑 → (𝑋 ∖ {𝑀}) ≈ 𝐾) |
11 | 2, 6, 10 | jca31 307 |
. . . 4
⊢ (𝜑 → (((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾)) |
12 | | zfz1isolem1.h |
. . . . 5
⊢ (𝜑 → ∀𝑦(((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦))) |
13 | | sseq1 3170 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑦 ⊆ ℤ ↔ (𝑋 ∖ {𝑀}) ⊆ ℤ)) |
14 | | eleq1 2233 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑦 ∈ Fin ↔ (𝑋 ∖ {𝑀}) ∈ Fin)) |
15 | 13, 14 | anbi12d 470 |
. . . . . . . . 9
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ↔ ((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin))) |
16 | | breq1 3992 |
. . . . . . . . 9
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑦 ≈ 𝐾 ↔ (𝑋 ∖ {𝑀}) ≈ 𝐾)) |
17 | 15, 16 | anbi12d 470 |
. . . . . . . 8
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) ↔ (((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾))) |
18 | | fveq2 5496 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (♯‘𝑦) = (♯‘(𝑋 ∖ {𝑀}))) |
19 | 18 | oveq2d 5869 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (1...(♯‘𝑦)) = (1...(♯‘(𝑋 ∖ {𝑀})))) |
20 | | isoeq4 5783 |
. . . . . . . . . . 11
⊢
((1...(♯‘𝑦)) = (1...(♯‘(𝑋 ∖ {𝑀}))) → (𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), 𝑦))) |
21 | 19, 20 | syl 14 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), 𝑦))) |
22 | | isoeq5 5784 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))) |
23 | 21, 22 | bitrd 187 |
. . . . . . . . 9
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))) |
24 | 23 | exbidv 1818 |
. . . . . . . 8
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ ∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))) |
25 | 17, 24 | imbi12d 233 |
. . . . . . 7
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → ((((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦)) ↔ ((((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))))) |
26 | 25 | spcgv 2817 |
. . . . . 6
⊢ ((𝑋 ∖ {𝑀}) ∈ Fin → (∀𝑦(((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦)) → ((((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))))) |
27 | 6, 26 | syl 14 |
. . . . 5
⊢ (𝜑 → (∀𝑦(((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦)) → ((((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))))) |
28 | 12, 27 | mpd 13 |
. . . 4
⊢ (𝜑 → ((((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))) |
29 | 11, 28 | mpd 13 |
. . 3
⊢ (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) |
30 | | isoeq1 5780 |
. . . 4
⊢ (𝑓 = 𝑔 → (𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})) ↔ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))) |
31 | 30 | cbvexv 1911 |
. . 3
⊢
(∃𝑓 𝑓 Isom < , <
((1...(♯‘(𝑋
∖ {𝑀}))), (𝑋 ∖ {𝑀})) ↔ ∃𝑔 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) |
32 | 29, 31 | sylib 121 |
. 2
⊢ (𝜑 → ∃𝑔 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) |
33 | | df-isom 5207 |
. . . . . . . . 9
⊢ (𝑔 Isom < , <
((1...(♯‘(𝑋
∖ {𝑀}))), (𝑋 ∖ {𝑀})) ↔ (𝑔:(1...(♯‘(𝑋 ∖ {𝑀})))–1-1-onto→(𝑋 ∖ {𝑀}) ∧ ∀𝑢 ∈ (1...(♯‘(𝑋 ∖ {𝑀})))∀𝑣 ∈ (1...(♯‘(𝑋 ∖ {𝑀})))(𝑢 < 𝑣 ↔ (𝑔‘𝑢) < (𝑔‘𝑣)))) |
34 | 33 | biimpi 119 |
. . . . . . . 8
⊢ (𝑔 Isom < , <
((1...(♯‘(𝑋
∖ {𝑀}))), (𝑋 ∖ {𝑀})) → (𝑔:(1...(♯‘(𝑋 ∖ {𝑀})))–1-1-onto→(𝑋 ∖ {𝑀}) ∧ ∀𝑢 ∈ (1...(♯‘(𝑋 ∖ {𝑀})))∀𝑣 ∈ (1...(♯‘(𝑋 ∖ {𝑀})))(𝑢 < 𝑣 ↔ (𝑔‘𝑢) < (𝑔‘𝑣)))) |
35 | 34 | adantl 275 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (𝑔:(1...(♯‘(𝑋 ∖ {𝑀})))–1-1-onto→(𝑋 ∖ {𝑀}) ∧ ∀𝑢 ∈ (1...(♯‘(𝑋 ∖ {𝑀})))∀𝑣 ∈ (1...(♯‘(𝑋 ∖ {𝑀})))(𝑢 < 𝑣 ↔ (𝑔‘𝑢) < (𝑔‘𝑣)))) |
36 | 35 | simpld 111 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → 𝑔:(1...(♯‘(𝑋 ∖ {𝑀})))–1-1-onto→(𝑋 ∖ {𝑀})) |
37 | | hashcl 10715 |
. . . . . . . . 9
⊢ (𝑋 ∈ Fin →
(♯‘𝑋) ∈
ℕ0) |
38 | 3, 37 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → (♯‘𝑋) ∈
ℕ0) |
39 | 38 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (♯‘𝑋) ∈
ℕ0) |
40 | 4 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → 𝑀 ∈ 𝑋) |
41 | | f1osng 5483 |
. . . . . . 7
⊢
(((♯‘𝑋)
∈ ℕ0 ∧ 𝑀 ∈ 𝑋) → {〈(♯‘𝑋), 𝑀〉}:{(♯‘𝑋)}–1-1-onto→{𝑀}) |
42 | 39, 40, 41 | syl2anc 409 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → {〈(♯‘𝑋), 𝑀〉}:{(♯‘𝑋)}–1-1-onto→{𝑀}) |
43 | | hashdifsn 10754 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ Fin ∧ 𝑀 ∈ 𝑋) → (♯‘(𝑋 ∖ {𝑀})) = ((♯‘𝑋) − 1)) |
44 | 3, 4, 43 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ (𝜑 → (♯‘(𝑋 ∖ {𝑀})) = ((♯‘𝑋) − 1)) |
45 | 44 | oveq1d 5868 |
. . . . . . . . . . 11
⊢ (𝜑 → ((♯‘(𝑋 ∖ {𝑀})) + 1) = (((♯‘𝑋) − 1) +
1)) |
46 | 38 | nn0cnd 9190 |
. . . . . . . . . . . 12
⊢ (𝜑 → (♯‘𝑋) ∈
ℂ) |
47 | | 1cnd 7936 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℂ) |
48 | 46, 47 | npcand 8234 |
. . . . . . . . . . 11
⊢ (𝜑 → (((♯‘𝑋) − 1) + 1) =
(♯‘𝑋)) |
49 | 45, 48 | eqtrd 2203 |
. . . . . . . . . 10
⊢ (𝜑 → ((♯‘(𝑋 ∖ {𝑀})) + 1) = (♯‘𝑋)) |
50 | 49 | sneqd 3596 |
. . . . . . . . 9
⊢ (𝜑 → {((♯‘(𝑋 ∖ {𝑀})) + 1)} = {(♯‘𝑋)}) |
51 | 50 | ineq2d 3328 |
. . . . . . . 8
⊢ (𝜑 →
((1...(♯‘(𝑋
∖ {𝑀}))) ∩
{((♯‘(𝑋 ∖
{𝑀})) + 1)}) =
((1...(♯‘(𝑋
∖ {𝑀}))) ∩
{(♯‘𝑋)})) |
52 | | fzp1disj 10036 |
. . . . . . . 8
⊢
((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {((♯‘(𝑋 ∖ {𝑀})) + 1)}) = ∅ |
53 | 51, 52 | eqtr3di 2218 |
. . . . . . 7
⊢ (𝜑 →
((1...(♯‘(𝑋
∖ {𝑀}))) ∩
{(♯‘𝑋)}) =
∅) |
54 | 53 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {(♯‘𝑋)}) = ∅) |
55 | | incom 3319 |
. . . . . . . 8
⊢ ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ({𝑀} ∩ (𝑋 ∖ {𝑀})) |
56 | | disjdif 3487 |
. . . . . . . 8
⊢ ({𝑀} ∩ (𝑋 ∖ {𝑀})) = ∅ |
57 | 55, 56 | eqtri 2191 |
. . . . . . 7
⊢ ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ∅ |
58 | 57 | a1i 9 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ∅) |
59 | | f1oun 5462 |
. . . . . 6
⊢ (((𝑔:(1...(♯‘(𝑋 ∖ {𝑀})))–1-1-onto→(𝑋 ∖ {𝑀}) ∧ {〈(♯‘𝑋), 𝑀〉}:{(♯‘𝑋)}–1-1-onto→{𝑀}) ∧ (((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {(♯‘𝑋)}) = ∅ ∧ ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ∅)) → (𝑔 ∪ {〈(♯‘𝑋), 𝑀〉}):((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})–1-1-onto→((𝑋 ∖ {𝑀}) ∪ {𝑀})) |
60 | 36, 42, 54, 58, 59 | syl22anc 1234 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (𝑔 ∪ {〈(♯‘𝑋), 𝑀〉}):((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})–1-1-onto→((𝑋 ∖ {𝑀}) ∪ {𝑀})) |
61 | 3, 4 | zfz1isolemsplit 10773 |
. . . . . . 7
⊢ (𝜑 → (1...(♯‘𝑋)) = ((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})) |
62 | | fidifsnid 6849 |
. . . . . . . . 9
⊢ ((𝑋 ∈ Fin ∧ 𝑀 ∈ 𝑋) → ((𝑋 ∖ {𝑀}) ∪ {𝑀}) = 𝑋) |
63 | 3, 4, 62 | syl2anc 409 |
. . . . . . . 8
⊢ (𝜑 → ((𝑋 ∖ {𝑀}) ∪ {𝑀}) = 𝑋) |
64 | 63 | eqcomd 2176 |
. . . . . . 7
⊢ (𝜑 → 𝑋 = ((𝑋 ∖ {𝑀}) ∪ {𝑀})) |
65 | | f1oeq23 5434 |
. . . . . . 7
⊢
(((1...(♯‘𝑋)) = ((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)}) ∧ 𝑋 = ((𝑋 ∖ {𝑀}) ∪ {𝑀})) → ((𝑔 ∪ {〈(♯‘𝑋), 𝑀〉}):(1...(♯‘𝑋))–1-1-onto→𝑋 ↔ (𝑔 ∪ {〈(♯‘𝑋), 𝑀〉}):((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})–1-1-onto→((𝑋 ∖ {𝑀}) ∪ {𝑀}))) |
66 | 61, 64, 65 | syl2anc 409 |
. . . . . 6
⊢ (𝜑 → ((𝑔 ∪ {〈(♯‘𝑋), 𝑀〉}):(1...(♯‘𝑋))–1-1-onto→𝑋 ↔ (𝑔 ∪ {〈(♯‘𝑋), 𝑀〉}):((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})–1-1-onto→((𝑋 ∖ {𝑀}) ∪ {𝑀}))) |
67 | 66 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ((𝑔 ∪ {〈(♯‘𝑋), 𝑀〉}):(1...(♯‘𝑋))–1-1-onto→𝑋 ↔ (𝑔 ∪ {〈(♯‘𝑋), 𝑀〉}):((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})–1-1-onto→((𝑋 ∖ {𝑀}) ∪ {𝑀}))) |
68 | 60, 67 | mpbird 166 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (𝑔 ∪ {〈(♯‘𝑋), 𝑀〉}):(1...(♯‘𝑋))–1-1-onto→𝑋) |
69 | 3 | ad2antrr 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑋 ∈ Fin) |
70 | 1 | ad2antrr 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑋 ⊆ ℤ) |
71 | 4 | ad2antrr 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑀 ∈ 𝑋) |
72 | | zfz1isolem1.m |
. . . . . . 7
⊢ (𝜑 → ∀𝑧 ∈ 𝑋 𝑧 ≤ 𝑀) |
73 | 72 | ad2antrr 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → ∀𝑧 ∈ 𝑋 𝑧 ≤ 𝑀) |
74 | | simplr 525 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) |
75 | | simprl 526 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑎 ∈ (1...(♯‘𝑋))) |
76 | | simprr 527 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑏 ∈ (1...(♯‘𝑋))) |
77 | 69, 70, 71, 73, 74, 75, 76 | zfz1isolemiso 10774 |
. . . . 5
⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → (𝑎 < 𝑏 ↔ ((𝑔 ∪ {〈(♯‘𝑋), 𝑀〉})‘𝑎) < ((𝑔 ∪ {〈(♯‘𝑋), 𝑀〉})‘𝑏))) |
78 | 77 | ralrimivva 2552 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ∀𝑎 ∈ (1...(♯‘𝑋))∀𝑏 ∈ (1...(♯‘𝑋))(𝑎 < 𝑏 ↔ ((𝑔 ∪ {〈(♯‘𝑋), 𝑀〉})‘𝑎) < ((𝑔 ∪ {〈(♯‘𝑋), 𝑀〉})‘𝑏))) |
79 | | df-isom 5207 |
. . . 4
⊢ ((𝑔 ∪
{〈(♯‘𝑋),
𝑀〉}) Isom < , <
((1...(♯‘𝑋)),
𝑋) ↔ ((𝑔 ∪
{〈(♯‘𝑋),
𝑀〉}):(1...(♯‘𝑋))–1-1-onto→𝑋 ∧ ∀𝑎 ∈
(1...(♯‘𝑋))∀𝑏 ∈ (1...(♯‘𝑋))(𝑎 < 𝑏 ↔ ((𝑔 ∪ {〈(♯‘𝑋), 𝑀〉})‘𝑎) < ((𝑔 ∪ {〈(♯‘𝑋), 𝑀〉})‘𝑏)))) |
80 | 68, 78, 79 | sylanbrc 415 |
. . 3
⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (𝑔 ∪ {〈(♯‘𝑋), 𝑀〉}) Isom < , <
((1...(♯‘𝑋)),
𝑋)) |
81 | | vex 2733 |
. . . . . . 7
⊢ 𝑔 ∈ V |
82 | 81 | a1i 9 |
. . . . . 6
⊢ (𝜑 → 𝑔 ∈ V) |
83 | | opexg 4213 |
. . . . . . . 8
⊢
(((♯‘𝑋)
∈ ℕ0 ∧ 𝑀 ∈ 𝑋) → 〈(♯‘𝑋), 𝑀〉 ∈ V) |
84 | 38, 4, 83 | syl2anc 409 |
. . . . . . 7
⊢ (𝜑 → 〈(♯‘𝑋), 𝑀〉 ∈ V) |
85 | | snexg 4170 |
. . . . . . 7
⊢
(〈(♯‘𝑋), 𝑀〉 ∈ V →
{〈(♯‘𝑋),
𝑀〉} ∈
V) |
86 | 84, 85 | syl 14 |
. . . . . 6
⊢ (𝜑 →
{〈(♯‘𝑋),
𝑀〉} ∈
V) |
87 | | unexg 4428 |
. . . . . 6
⊢ ((𝑔 ∈ V ∧
{〈(♯‘𝑋),
𝑀〉} ∈ V) →
(𝑔 ∪
{〈(♯‘𝑋),
𝑀〉}) ∈
V) |
88 | 82, 86, 87 | syl2anc 409 |
. . . . 5
⊢ (𝜑 → (𝑔 ∪ {〈(♯‘𝑋), 𝑀〉}) ∈ V) |
89 | | isoeq1 5780 |
. . . . . 6
⊢ (𝑓 = (𝑔 ∪ {〈(♯‘𝑋), 𝑀〉}) → (𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋) ↔ (𝑔 ∪ {〈(♯‘𝑋), 𝑀〉}) Isom < , <
((1...(♯‘𝑋)),
𝑋))) |
90 | 89 | spcegv 2818 |
. . . . 5
⊢ ((𝑔 ∪
{〈(♯‘𝑋),
𝑀〉}) ∈ V →
((𝑔 ∪
{〈(♯‘𝑋),
𝑀〉}) Isom < , <
((1...(♯‘𝑋)),
𝑋) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋))) |
91 | 88, 90 | syl 14 |
. . . 4
⊢ (𝜑 → ((𝑔 ∪ {〈(♯‘𝑋), 𝑀〉}) Isom < , <
((1...(♯‘𝑋)),
𝑋) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋))) |
92 | 91 | adantr 274 |
. . 3
⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ((𝑔 ∪ {〈(♯‘𝑋), 𝑀〉}) Isom < , <
((1...(♯‘𝑋)),
𝑋) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋))) |
93 | 80, 92 | mpd 13 |
. 2
⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋)) |
94 | 32, 93 | exlimddv 1891 |
1
⊢ (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋)) |