Proof of Theorem fz1isolem
Step | Hyp | Ref
| Expression |
1 | | hashcl 13956 |
. . . . . . . . 9
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℕ0) |
2 | 1 | adantl 485 |
. . . . . . . 8
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (♯‘𝐴) ∈
ℕ0) |
3 | | nnuz 12507 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
4 | | 1z 12237 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℤ |
5 | | fz1iso.1 |
. . . . . . . . . . . . 13
⊢ 𝐺 = (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω) |
6 | 4, 5 | om2uzisoi 13559 |
. . . . . . . . . . . 12
⊢ 𝐺 Isom E , < (ω,
(ℤ≥‘1)) |
7 | | isoeq5 7152 |
. . . . . . . . . . . 12
⊢ (ℕ
= (ℤ≥‘1) → (𝐺 Isom E , < (ω, ℕ) ↔
𝐺 Isom E , < (ω,
(ℤ≥‘1)))) |
8 | 6, 7 | mpbiri 261 |
. . . . . . . . . . 11
⊢ (ℕ
= (ℤ≥‘1) → 𝐺 Isom E , < (ω,
ℕ)) |
9 | 3, 8 | ax-mp 5 |
. . . . . . . . . 10
⊢ 𝐺 Isom E , < (ω,
ℕ) |
10 | | isocnv 7161 |
. . . . . . . . . 10
⊢ (𝐺 Isom E , < (ω,
ℕ) → ◡𝐺 Isom < , E (ℕ,
ω)) |
11 | 9, 10 | ax-mp 5 |
. . . . . . . . 9
⊢ ◡𝐺 Isom < , E (ℕ,
ω) |
12 | | nn0p1nn 12159 |
. . . . . . . . 9
⊢
((♯‘𝐴)
∈ ℕ0 → ((♯‘𝐴) + 1) ∈ ℕ) |
13 | | fz1iso.2 |
. . . . . . . . . 10
⊢ 𝐵 = (ℕ ∩ (◡ < “ {((♯‘𝐴) + 1)})) |
14 | | fz1iso.3 |
. . . . . . . . . . 11
⊢ 𝐶 = (ω ∩ (◡𝐺‘((♯‘𝐴) + 1))) |
15 | | fvex 6752 |
. . . . . . . . . . . . 13
⊢ (◡𝐺‘((♯‘𝐴) + 1)) ∈ V |
16 | 15 | epini 5982 |
. . . . . . . . . . . 12
⊢ (◡ E “ {(◡𝐺‘((♯‘𝐴) + 1))}) = (◡𝐺‘((♯‘𝐴) + 1)) |
17 | 16 | ineq2i 4141 |
. . . . . . . . . . 11
⊢ (ω
∩ (◡ E “ {(◡𝐺‘((♯‘𝐴) + 1))})) = (ω ∩ (◡𝐺‘((♯‘𝐴) + 1))) |
18 | 14, 17 | eqtr4i 2770 |
. . . . . . . . . 10
⊢ 𝐶 = (ω ∩ (◡ E “ {(◡𝐺‘((♯‘𝐴) + 1))})) |
19 | 13, 18 | isoini2 7170 |
. . . . . . . . 9
⊢ ((◡𝐺 Isom < , E (ℕ, ω) ∧
((♯‘𝐴) + 1)
∈ ℕ) → (◡𝐺 ↾ 𝐵) Isom < , E (𝐵, 𝐶)) |
20 | 11, 12, 19 | sylancr 590 |
. . . . . . . 8
⊢
((♯‘𝐴)
∈ ℕ0 → (◡𝐺 ↾ 𝐵) Isom < , E (𝐵, 𝐶)) |
21 | 2, 20 | syl 17 |
. . . . . . 7
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (◡𝐺 ↾ 𝐵) Isom < , E (𝐵, 𝐶)) |
22 | | nnz 12229 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ ℕ → 𝑓 ∈
ℤ) |
23 | 2 | nn0zd 12310 |
. . . . . . . . . . . . 13
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (♯‘𝐴) ∈
ℤ) |
24 | | eluz 12482 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ ℤ ∧
(♯‘𝐴) ∈
ℤ) → ((♯‘𝐴) ∈ (ℤ≥‘𝑓) ↔ 𝑓 ≤ (♯‘𝐴))) |
25 | 22, 23, 24 | syl2anr 600 |
. . . . . . . . . . . 12
⊢ (((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → ((♯‘𝐴) ∈
(ℤ≥‘𝑓) ↔ 𝑓 ≤ (♯‘𝐴))) |
26 | | zleltp1 12258 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ ℤ ∧
(♯‘𝐴) ∈
ℤ) → (𝑓 ≤
(♯‘𝐴) ↔
𝑓 <
((♯‘𝐴) +
1))) |
27 | 22, 23, 26 | syl2anr 600 |
. . . . . . . . . . . . 13
⊢ (((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → (𝑓 ≤ (♯‘𝐴) ↔ 𝑓 < ((♯‘𝐴) + 1))) |
28 | | ovex 7268 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝐴) +
1) ∈ V |
29 | | vex 3427 |
. . . . . . . . . . . . . . 15
⊢ 𝑓 ∈ V |
30 | 29 | eliniseg 5980 |
. . . . . . . . . . . . . 14
⊢
(((♯‘𝐴)
+ 1) ∈ V → (𝑓
∈ (◡ < “
{((♯‘𝐴) + 1)})
↔ 𝑓 <
((♯‘𝐴) +
1))) |
31 | 28, 30 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ (◡ < “ {((♯‘𝐴) + 1)}) ↔ 𝑓 < ((♯‘𝐴) + 1)) |
32 | 27, 31 | bitr4di 292 |
. . . . . . . . . . . 12
⊢ (((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → (𝑓 ≤ (♯‘𝐴) ↔ 𝑓 ∈ (◡ < “ {((♯‘𝐴) + 1)}))) |
33 | 25, 32 | bitr2d 283 |
. . . . . . . . . . 11
⊢ (((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → (𝑓 ∈ (◡ < “ {((♯‘𝐴) + 1)}) ↔
(♯‘𝐴) ∈
(ℤ≥‘𝑓))) |
34 | 33 | pm5.32da 582 |
. . . . . . . . . 10
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ((𝑓 ∈ ℕ ∧ 𝑓 ∈ (◡ < “ {((♯‘𝐴) + 1)})) ↔ (𝑓 ∈ ℕ ∧
(♯‘𝐴) ∈
(ℤ≥‘𝑓)))) |
35 | 13 | elin2 4128 |
. . . . . . . . . 10
⊢ (𝑓 ∈ 𝐵 ↔ (𝑓 ∈ ℕ ∧ 𝑓 ∈ (◡ < “ {((♯‘𝐴) + 1)}))) |
36 | | elfzuzb 13136 |
. . . . . . . . . . 11
⊢ (𝑓 ∈
(1...(♯‘𝐴))
↔ (𝑓 ∈
(ℤ≥‘1) ∧ (♯‘𝐴) ∈ (ℤ≥‘𝑓))) |
37 | | elnnuz 12508 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ ℕ ↔ 𝑓 ∈
(ℤ≥‘1)) |
38 | 37 | anbi1i 627 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ ℕ ∧
(♯‘𝐴) ∈
(ℤ≥‘𝑓)) ↔ (𝑓 ∈ (ℤ≥‘1)
∧ (♯‘𝐴)
∈ (ℤ≥‘𝑓))) |
39 | 36, 38 | bitr4i 281 |
. . . . . . . . . 10
⊢ (𝑓 ∈
(1...(♯‘𝐴))
↔ (𝑓 ∈ ℕ
∧ (♯‘𝐴)
∈ (ℤ≥‘𝑓))) |
40 | 34, 35, 39 | 3bitr4g 317 |
. . . . . . . . 9
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (𝑓 ∈ 𝐵 ↔ 𝑓 ∈ (1...(♯‘𝐴)))) |
41 | 40 | eqrdv 2737 |
. . . . . . . 8
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝐵 = (1...(♯‘𝐴))) |
42 | | isoeq4 7151 |
. . . . . . . 8
⊢ (𝐵 = (1...(♯‘𝐴)) → ((◡𝐺 ↾ 𝐵) Isom < , E (𝐵, 𝐶) ↔ (◡𝐺 ↾ 𝐵) Isom < , E ((1...(♯‘𝐴)), 𝐶))) |
43 | 41, 42 | syl 17 |
. . . . . . 7
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ((◡𝐺 ↾ 𝐵) Isom < , E (𝐵, 𝐶) ↔ (◡𝐺 ↾ 𝐵) Isom < , E ((1...(♯‘𝐴)), 𝐶))) |
44 | 21, 43 | mpbid 235 |
. . . . . 6
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (◡𝐺 ↾ 𝐵) Isom < , E ((1...(♯‘𝐴)), 𝐶)) |
45 | | fz1iso.4 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑂 = OrdIso(𝑅, 𝐴) |
46 | 45 | oion 9182 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ Fin → dom 𝑂 ∈ On) |
47 | 46 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom 𝑂 ∈ On) |
48 | | simpr 488 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝐴 ∈ Fin) |
49 | | wofi 8950 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝑅 We 𝐴) |
50 | 45 | oien 9184 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ Fin ∧ 𝑅 We 𝐴) → dom 𝑂 ≈ 𝐴) |
51 | 48, 49, 50 | syl2anc 587 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom 𝑂 ≈ 𝐴) |
52 | | enfii 8891 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ Fin ∧ dom 𝑂 ≈ 𝐴) → dom 𝑂 ∈ Fin) |
53 | 48, 51, 52 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom 𝑂 ∈ Fin) |
54 | 47, 53 | elind 4125 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom 𝑂 ∈ (On ∩ Fin)) |
55 | | onfin2 8901 |
. . . . . . . . . . . . . . 15
⊢ ω =
(On ∩ Fin) |
56 | 54, 55 | eleqtrrdi 2851 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom 𝑂 ∈ ω) |
57 | | eqid 2739 |
. . . . . . . . . . . . . . . 16
⊢
(rec((𝑛 ∈ V
↦ (𝑛 + 1)), 0)
↾ ω) = (rec((𝑛
∈ V ↦ (𝑛 + 1)),
0) ↾ ω) |
58 | | 0z 12217 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℤ |
59 | 5, 57, 4, 58 | uzrdgxfr 13572 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝑂 ∈ ω →
(𝐺‘dom 𝑂) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + (1 −
0))) |
60 | | 1m0e1 11981 |
. . . . . . . . . . . . . . . 16
⊢ (1
− 0) = 1 |
61 | 60 | oveq2i 7246 |
. . . . . . . . . . . . . . 15
⊢
(((rec((𝑛 ∈ V
↦ (𝑛 + 1)), 0)
↾ ω)‘dom 𝑂) + (1 − 0)) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾
ω)‘dom 𝑂) +
1) |
62 | 59, 61 | eqtrdi 2796 |
. . . . . . . . . . . . . 14
⊢ (dom
𝑂 ∈ ω →
(𝐺‘dom 𝑂) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1)) |
63 | 56, 62 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (𝐺‘dom 𝑂) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1)) |
64 | 51 | ensymd 8705 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝐴 ≈ dom 𝑂) |
65 | | cardennn 9629 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ≈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → (card‘𝐴) = dom 𝑂) |
66 | 64, 56, 65 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (card‘𝐴) = dom 𝑂) |
67 | 66 | fveq2d 6743 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾
ω)‘(card‘𝐴)) = ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂)) |
68 | 57 | hashgval 13932 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ Fin → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾
ω)‘(card‘𝐴)) = (♯‘𝐴)) |
69 | 68 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾
ω)‘(card‘𝐴)) = (♯‘𝐴)) |
70 | 67, 69 | eqtr3d 2781 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾
ω)‘dom 𝑂) =
(♯‘𝐴)) |
71 | 70 | oveq1d 7250 |
. . . . . . . . . . . . 13
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾
ω)‘dom 𝑂) + 1)
= ((♯‘𝐴) +
1)) |
72 | 63, 71 | eqtrd 2779 |
. . . . . . . . . . . 12
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (𝐺‘dom 𝑂) = ((♯‘𝐴) + 1)) |
73 | 72 | fveq2d 6743 |
. . . . . . . . . . 11
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (◡𝐺‘(𝐺‘dom 𝑂)) = (◡𝐺‘((♯‘𝐴) + 1))) |
74 | | isof1o 7154 |
. . . . . . . . . . . . 13
⊢ (𝐺 Isom E , < (ω,
ℕ) → 𝐺:ω–1-1-onto→ℕ) |
75 | 9, 74 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ 𝐺:ω–1-1-onto→ℕ |
76 | | f1ocnvfv1 7109 |
. . . . . . . . . . . 12
⊢ ((𝐺:ω–1-1-onto→ℕ ∧ dom 𝑂 ∈ ω) → (◡𝐺‘(𝐺‘dom 𝑂)) = dom 𝑂) |
77 | 75, 56, 76 | sylancr 590 |
. . . . . . . . . . 11
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (◡𝐺‘(𝐺‘dom 𝑂)) = dom 𝑂) |
78 | 73, 77 | eqtr3d 2781 |
. . . . . . . . . 10
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (◡𝐺‘((♯‘𝐴) + 1)) = dom 𝑂) |
79 | 78 | ineq2d 4144 |
. . . . . . . . 9
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (ω ∩ (◡𝐺‘((♯‘𝐴) + 1))) = (ω ∩ dom 𝑂)) |
80 | | ordom 7676 |
. . . . . . . . . . 11
⊢ Ord
ω |
81 | | ordelss 6250 |
. . . . . . . . . . 11
⊢ ((Ord
ω ∧ dom 𝑂 ∈
ω) → dom 𝑂
⊆ ω) |
82 | 80, 56, 81 | sylancr 590 |
. . . . . . . . . 10
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom 𝑂 ⊆ ω) |
83 | | sseqin2 4147 |
. . . . . . . . . 10
⊢ (dom
𝑂 ⊆ ω ↔
(ω ∩ dom 𝑂) = dom
𝑂) |
84 | 82, 83 | sylib 221 |
. . . . . . . . 9
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (ω ∩ dom 𝑂) = dom 𝑂) |
85 | 79, 84 | eqtrd 2779 |
. . . . . . . 8
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (ω ∩ (◡𝐺‘((♯‘𝐴) + 1))) = dom 𝑂) |
86 | 14, 85 | eqtrid 2791 |
. . . . . . 7
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝐶 = dom 𝑂) |
87 | | isoeq5 7152 |
. . . . . . 7
⊢ (𝐶 = dom 𝑂 → ((◡𝐺 ↾ 𝐵) Isom < , E ((1...(♯‘𝐴)), 𝐶) ↔ (◡𝐺 ↾ 𝐵) Isom < , E ((1...(♯‘𝐴)), dom 𝑂))) |
88 | 86, 87 | syl 17 |
. . . . . 6
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ((◡𝐺 ↾ 𝐵) Isom < , E ((1...(♯‘𝐴)), 𝐶) ↔ (◡𝐺 ↾ 𝐵) Isom < , E ((1...(♯‘𝐴)), dom 𝑂))) |
89 | 44, 88 | mpbid 235 |
. . . . 5
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (◡𝐺 ↾ 𝐵) Isom < , E ((1...(♯‘𝐴)), dom 𝑂)) |
90 | 45 | oiiso 9183 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝑅 We 𝐴) → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴)) |
91 | 48, 49, 90 | syl2anc 587 |
. . . . 5
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴)) |
92 | | isotr 7167 |
. . . . 5
⊢ (((◡𝐺 ↾ 𝐵) Isom < , E ((1...(♯‘𝐴)), dom 𝑂) ∧ 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴)) → (𝑂 ∘ (◡𝐺 ↾ 𝐵)) Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴)) |
93 | 89, 91, 92 | syl2anc 587 |
. . . 4
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (𝑂 ∘ (◡𝐺 ↾ 𝐵)) Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴)) |
94 | | isof1o 7154 |
. . . 4
⊢ ((𝑂 ∘ (◡𝐺 ↾ 𝐵)) Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴) → (𝑂 ∘ (◡𝐺 ↾ 𝐵)):(1...(♯‘𝐴))–1-1-onto→𝐴) |
95 | | f1of 6683 |
. . . 4
⊢ ((𝑂 ∘ (◡𝐺 ↾ 𝐵)):(1...(♯‘𝐴))–1-1-onto→𝐴 → (𝑂 ∘ (◡𝐺 ↾ 𝐵)):(1...(♯‘𝐴))⟶𝐴) |
96 | 93, 94, 95 | 3syl 18 |
. . 3
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (𝑂 ∘ (◡𝐺 ↾ 𝐵)):(1...(♯‘𝐴))⟶𝐴) |
97 | | fzfid 13578 |
. . 3
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) →
(1...(♯‘𝐴))
∈ Fin) |
98 | 96, 97 | fexd 7065 |
. 2
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (𝑂 ∘ (◡𝐺 ↾ 𝐵)) ∈ V) |
99 | | isoeq1 7148 |
. 2
⊢ (𝑓 = (𝑂 ∘ (◡𝐺 ↾ 𝐵)) → (𝑓 Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴) ↔ (𝑂 ∘ (◡𝐺 ↾ 𝐵)) Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴))) |
100 | 98, 93, 99 | spcedv 3528 |
1
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ∃𝑓 𝑓 Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴)) |