Step | Hyp | Ref
| Expression |
1 | | zfz1isolem1.xz |
. . . . . 6
⊢ (𝜑 → 𝑋 ⊆ ℤ) |
2 | 1 | ssdifssd 3245 |
. . . . 5
⊢ (𝜑 → (𝑋 ∖ {𝑀}) ⊆ ℤ) |
3 | | zfz1isolem1.xf |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ Fin) |
4 | | zfz1isolem1.mx |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ 𝑋) |
5 | | diffisn 6839 |
. . . . . 6
⊢ ((𝑋 ∈ Fin ∧ 𝑀 ∈ 𝑋) → (𝑋 ∖ {𝑀}) ∈ Fin) |
6 | 3, 4, 5 | syl2anc 409 |
. . . . 5
⊢ (𝜑 → (𝑋 ∖ {𝑀}) ∈ Fin) |
7 | | zfz1isolem1.k |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ ω) |
8 | | zfz1isolem1.xs |
. . . . . 6
⊢ (𝜑 → 𝑋 ≈ suc 𝐾) |
9 | | dif1en 6825 |
. . . . . 6
⊢ ((𝐾 ∈ ω ∧ 𝑋 ≈ suc 𝐾 ∧ 𝑀 ∈ 𝑋) → (𝑋 ∖ {𝑀}) ≈ 𝐾) |
10 | 7, 8, 4, 9 | syl3anc 1220 |
. . . . 5
⊢ (𝜑 → (𝑋 ∖ {𝑀}) ≈ 𝐾) |
11 | 2, 6, 10 | jca31 307 |
. . . 4
⊢ (𝜑 → (((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾)) |
12 | | zfz1isolem1.h |
. . . . 5
⊢ (𝜑 → ∀𝑦(((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦))) |
13 | | sseq1 3151 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑦 ⊆ ℤ ↔ (𝑋 ∖ {𝑀}) ⊆ ℤ)) |
14 | | eleq1 2220 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑦 ∈ Fin ↔ (𝑋 ∖ {𝑀}) ∈ Fin)) |
15 | 13, 14 | anbi12d 465 |
. . . . . . . . 9
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → ((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ↔ ((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin))) |
16 | | breq1 3969 |
. . . . . . . . 9
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑦 ≈ 𝐾 ↔ (𝑋 ∖ {𝑀}) ≈ 𝐾)) |
17 | 15, 16 | anbi12d 465 |
. . . . . . . 8
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) ↔ (((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾))) |
18 | | fveq2 5469 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (♯‘𝑦) = (♯‘(𝑋 ∖ {𝑀}))) |
19 | 18 | oveq2d 5841 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (1...(♯‘𝑦)) = (1...(♯‘(𝑋 ∖ {𝑀})))) |
20 | | isoeq4 5755 |
. . . . . . . . . . 11
⊢
((1...(♯‘𝑦)) = (1...(♯‘(𝑋 ∖ {𝑀}))) → (𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), 𝑦))) |
21 | 19, 20 | syl 14 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), 𝑦))) |
22 | | isoeq5 5756 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))) |
23 | 21, 22 | bitrd 187 |
. . . . . . . . 9
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))) |
24 | 23 | exbidv 1805 |
. . . . . . . 8
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → (∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦) ↔ ∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))) |
25 | 17, 24 | imbi12d 233 |
. . . . . . 7
⊢ (𝑦 = (𝑋 ∖ {𝑀}) → ((((𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ 𝑦 ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑦)), 𝑦)) ↔ ((((𝑋 ∖ {𝑀}) ⊆ ℤ ∧ (𝑋 ∖ {𝑀}) ∈ Fin) ∧ (𝑋 ∖ {𝑀}) ≈ 𝐾) → ∃𝑓 𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))))) |
26 | 25 | spcgv 2799 |
. . . . . 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 5752 |
. . . 4
⊢ (𝑓 = 𝑔 → (𝑓 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})) ↔ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀})))) |
31 | 30 | cbvexv 1898 |
. . 3
⊢
(∃𝑓 𝑓 Isom < , <
((1...(♯‘(𝑋
∖ {𝑀}))), (𝑋 ∖ {𝑀})) ↔ ∃𝑔 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) |
32 | 29, 31 | sylib 121 |
. 2
⊢ (𝜑 → ∃𝑔 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) |
33 | | df-isom 5180 |
. . . . . . . . 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 10659 |
. . . . . . . . 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 5456 |
. . . . . . 7
⊢
(((♯‘𝑋)
∈ ℕ0 ∧ 𝑀 ∈ 𝑋) → {〈(♯‘𝑋), 𝑀〉}:{(♯‘𝑋)}–1-1-onto→{𝑀}) |
42 | 39, 40, 41 | syl2anc 409 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → {〈(♯‘𝑋), 𝑀〉}:{(♯‘𝑋)}–1-1-onto→{𝑀}) |
43 | | fzp1disj 9983 |
. . . . . . . 8
⊢
((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {((♯‘(𝑋 ∖ {𝑀})) + 1)}) = ∅ |
44 | | hashdifsn 10697 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ Fin ∧ 𝑀 ∈ 𝑋) → (♯‘(𝑋 ∖ {𝑀})) = ((♯‘𝑋) − 1)) |
45 | 3, 4, 44 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ (𝜑 → (♯‘(𝑋 ∖ {𝑀})) = ((♯‘𝑋) − 1)) |
46 | 45 | oveq1d 5840 |
. . . . . . . . . . 11
⊢ (𝜑 → ((♯‘(𝑋 ∖ {𝑀})) + 1) = (((♯‘𝑋) − 1) +
1)) |
47 | 38 | nn0cnd 9146 |
. . . . . . . . . . . 12
⊢ (𝜑 → (♯‘𝑋) ∈
ℂ) |
48 | | 1cnd 7895 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℂ) |
49 | 47, 48 | npcand 8191 |
. . . . . . . . . . 11
⊢ (𝜑 → (((♯‘𝑋) − 1) + 1) =
(♯‘𝑋)) |
50 | 46, 49 | eqtrd 2190 |
. . . . . . . . . 10
⊢ (𝜑 → ((♯‘(𝑋 ∖ {𝑀})) + 1) = (♯‘𝑋)) |
51 | 50 | sneqd 3573 |
. . . . . . . . 9
⊢ (𝜑 → {((♯‘(𝑋 ∖ {𝑀})) + 1)} = {(♯‘𝑋)}) |
52 | 51 | ineq2d 3308 |
. . . . . . . 8
⊢ (𝜑 →
((1...(♯‘(𝑋
∖ {𝑀}))) ∩
{((♯‘(𝑋 ∖
{𝑀})) + 1)}) =
((1...(♯‘(𝑋
∖ {𝑀}))) ∩
{(♯‘𝑋)})) |
53 | 43, 52 | syl5reqr 2205 |
. . . . . . 7
⊢ (𝜑 →
((1...(♯‘(𝑋
∖ {𝑀}))) ∩
{(♯‘𝑋)}) =
∅) |
54 | 53 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {(♯‘𝑋)}) = ∅) |
55 | | incom 3299 |
. . . . . . . 8
⊢ ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ({𝑀} ∩ (𝑋 ∖ {𝑀})) |
56 | | disjdif 3466 |
. . . . . . . 8
⊢ ({𝑀} ∩ (𝑋 ∖ {𝑀})) = ∅ |
57 | 55, 56 | eqtri 2178 |
. . . . . . 7
⊢ ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ∅ |
58 | 57 | a1i 9 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ∅) |
59 | | f1oun 5435 |
. . . . . 6
⊢ (((𝑔:(1...(♯‘(𝑋 ∖ {𝑀})))–1-1-onto→(𝑋 ∖ {𝑀}) ∧ {〈(♯‘𝑋), 𝑀〉}:{(♯‘𝑋)}–1-1-onto→{𝑀}) ∧ (((1...(♯‘(𝑋 ∖ {𝑀}))) ∩ {(♯‘𝑋)}) = ∅ ∧ ((𝑋 ∖ {𝑀}) ∩ {𝑀}) = ∅)) → (𝑔 ∪ {〈(♯‘𝑋), 𝑀〉}):((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})–1-1-onto→((𝑋 ∖ {𝑀}) ∪ {𝑀})) |
60 | 36, 42, 54, 58, 59 | syl22anc 1221 |
. . . . 5
⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (𝑔 ∪ {〈(♯‘𝑋), 𝑀〉}):((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})–1-1-onto→((𝑋 ∖ {𝑀}) ∪ {𝑀})) |
61 | 3, 4 | zfz1isolemsplit 10713 |
. . . . . . 7
⊢ (𝜑 → (1...(♯‘𝑋)) = ((1...(♯‘(𝑋 ∖ {𝑀}))) ∪ {(♯‘𝑋)})) |
62 | | fidifsnid 6817 |
. . . . . . . . 9
⊢ ((𝑋 ∈ Fin ∧ 𝑀 ∈ 𝑋) → ((𝑋 ∖ {𝑀}) ∪ {𝑀}) = 𝑋) |
63 | 3, 4, 62 | syl2anc 409 |
. . . . . . . 8
⊢ (𝜑 → ((𝑋 ∖ {𝑀}) ∪ {𝑀}) = 𝑋) |
64 | 63 | eqcomd 2163 |
. . . . . . 7
⊢ (𝜑 → 𝑋 = ((𝑋 ∖ {𝑀}) ∪ {𝑀})) |
65 | | f1oeq23 5407 |
. . . . . . 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 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑋 ∈ Fin) |
70 | 1 | ad2antrr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑋 ⊆ ℤ) |
71 | 4 | ad2antrr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑀 ∈ 𝑋) |
72 | | zfz1isolem1.m |
. . . . . . 7
⊢ (𝜑 → ∀𝑧 ∈ 𝑋 𝑧 ≤ 𝑀) |
73 | 72 | ad2antrr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → ∀𝑧 ∈ 𝑋 𝑧 ≤ 𝑀) |
74 | | simplr 520 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) |
75 | | simprl 521 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑎 ∈ (1...(♯‘𝑋))) |
76 | | simprr 522 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → 𝑏 ∈ (1...(♯‘𝑋))) |
77 | 69, 70, 71, 73, 74, 75, 76 | zfz1isolemiso 10714 |
. . . . 5
⊢ (((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) ∧ (𝑎 ∈ (1...(♯‘𝑋)) ∧ 𝑏 ∈ (1...(♯‘𝑋)))) → (𝑎 < 𝑏 ↔ ((𝑔 ∪ {〈(♯‘𝑋), 𝑀〉})‘𝑎) < ((𝑔 ∪ {〈(♯‘𝑋), 𝑀〉})‘𝑏))) |
78 | 77 | ralrimivva 2539 |
. . . 4
⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → ∀𝑎 ∈ (1...(♯‘𝑋))∀𝑏 ∈ (1...(♯‘𝑋))(𝑎 < 𝑏 ↔ ((𝑔 ∪ {〈(♯‘𝑋), 𝑀〉})‘𝑎) < ((𝑔 ∪ {〈(♯‘𝑋), 𝑀〉})‘𝑏))) |
79 | | df-isom 5180 |
. . . 4
⊢ ((𝑔 ∪
{〈(♯‘𝑋),
𝑀〉}) Isom < , <
((1...(♯‘𝑋)),
𝑋) ↔ ((𝑔 ∪
{〈(♯‘𝑋),
𝑀〉}):(1...(♯‘𝑋))–1-1-onto→𝑋 ∧ ∀𝑎 ∈
(1...(♯‘𝑋))∀𝑏 ∈ (1...(♯‘𝑋))(𝑎 < 𝑏 ↔ ((𝑔 ∪ {〈(♯‘𝑋), 𝑀〉})‘𝑎) < ((𝑔 ∪ {〈(♯‘𝑋), 𝑀〉})‘𝑏)))) |
80 | 68, 78, 79 | sylanbrc 414 |
. . 3
⊢ ((𝜑 ∧ 𝑔 Isom < , < ((1...(♯‘(𝑋 ∖ {𝑀}))), (𝑋 ∖ {𝑀}))) → (𝑔 ∪ {〈(♯‘𝑋), 𝑀〉}) Isom < , <
((1...(♯‘𝑋)),
𝑋)) |
81 | | vex 2715 |
. . . . . . 7
⊢ 𝑔 ∈ V |
82 | 81 | a1i 9 |
. . . . . 6
⊢ (𝜑 → 𝑔 ∈ V) |
83 | | opexg 4189 |
. . . . . . . 8
⊢
(((♯‘𝑋)
∈ ℕ0 ∧ 𝑀 ∈ 𝑋) → 〈(♯‘𝑋), 𝑀〉 ∈ V) |
84 | 38, 4, 83 | syl2anc 409 |
. . . . . . 7
⊢ (𝜑 → 〈(♯‘𝑋), 𝑀〉 ∈ V) |
85 | | snexg 4146 |
. . . . . . 7
⊢
(〈(♯‘𝑋), 𝑀〉 ∈ V →
{〈(♯‘𝑋),
𝑀〉} ∈
V) |
86 | 84, 85 | syl 14 |
. . . . . 6
⊢ (𝜑 →
{〈(♯‘𝑋),
𝑀〉} ∈
V) |
87 | | unexg 4404 |
. . . . . 6
⊢ ((𝑔 ∈ V ∧
{〈(♯‘𝑋),
𝑀〉} ∈ V) →
(𝑔 ∪
{〈(♯‘𝑋),
𝑀〉}) ∈
V) |
88 | 82, 86, 87 | syl2anc 409 |
. . . . 5
⊢ (𝜑 → (𝑔 ∪ {〈(♯‘𝑋), 𝑀〉}) ∈ V) |
89 | | isoeq1 5752 |
. . . . . 6
⊢ (𝑓 = (𝑔 ∪ {〈(♯‘𝑋), 𝑀〉}) → (𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋) ↔ (𝑔 ∪ {〈(♯‘𝑋), 𝑀〉}) Isom < , <
((1...(♯‘𝑋)),
𝑋))) |
90 | 89 | spcegv 2800 |
. . . . 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 1878 |
1
⊢ (𝜑 → ∃𝑓 𝑓 Isom < , < ((1...(♯‘𝑋)), 𝑋)) |