Proof of Theorem fz1isolem
Step | Hyp | Ref
| Expression |
1 | | hashcl 13009 |
. . . . . . . . 9
⊢ (𝐴 ∈ Fin →
(#‘𝐴) ∈
ℕ0) |
2 | 1 | adantl 481 |
. . . . . . . 8
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (#‘𝐴) ∈
ℕ0) |
3 | | nnuz 11599 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
4 | | 1z 11284 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℤ |
5 | | fz1iso.1 |
. . . . . . . . . . . . 13
⊢ 𝐺 = (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω) |
6 | 4, 5 | om2uzisoi 12615 |
. . . . . . . . . . . 12
⊢ 𝐺 Isom E , < (ω,
(ℤ≥‘1)) |
7 | | isoeq5 6471 |
. . . . . . . . . . . 12
⊢ (ℕ
= (ℤ≥‘1) → (𝐺 Isom E , < (ω, ℕ) ↔
𝐺 Isom E , < (ω,
(ℤ≥‘1)))) |
8 | 6, 7 | mpbiri 247 |
. . . . . . . . . . 11
⊢ (ℕ
= (ℤ≥‘1) → 𝐺 Isom E , < (ω,
ℕ)) |
9 | 3, 8 | ax-mp 5 |
. . . . . . . . . 10
⊢ 𝐺 Isom E , < (ω,
ℕ) |
10 | | isocnv 6480 |
. . . . . . . . . 10
⊢ (𝐺 Isom E , < (ω,
ℕ) → ◡𝐺 Isom < , E (ℕ,
ω)) |
11 | 9, 10 | ax-mp 5 |
. . . . . . . . 9
⊢ ◡𝐺 Isom < , E (ℕ,
ω) |
12 | | nn0p1nn 11209 |
. . . . . . . . 9
⊢
((#‘𝐴) ∈
ℕ0 → ((#‘𝐴) + 1) ∈ ℕ) |
13 | | fz1iso.2 |
. . . . . . . . . 10
⊢ 𝐵 = (ℕ ∩ (◡ < “ {((#‘𝐴) + 1)})) |
14 | | fz1iso.3 |
. . . . . . . . . . 11
⊢ 𝐶 = (ω ∩ (◡𝐺‘((#‘𝐴) + 1))) |
15 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢ (◡𝐺‘((#‘𝐴) + 1)) ∈ V |
16 | 15 | epini 5414 |
. . . . . . . . . . . 12
⊢ (◡ E “ {(◡𝐺‘((#‘𝐴) + 1))}) = (◡𝐺‘((#‘𝐴) + 1)) |
17 | 16 | ineq2i 3773 |
. . . . . . . . . . 11
⊢ (ω
∩ (◡ E “ {(◡𝐺‘((#‘𝐴) + 1))})) = (ω ∩ (◡𝐺‘((#‘𝐴) + 1))) |
18 | 14, 17 | eqtr4i 2635 |
. . . . . . . . . 10
⊢ 𝐶 = (ω ∩ (◡ E “ {(◡𝐺‘((#‘𝐴) + 1))})) |
19 | 13, 18 | isoini2 6489 |
. . . . . . . . 9
⊢ ((◡𝐺 Isom < , E (ℕ, ω) ∧
((#‘𝐴) + 1) ∈
ℕ) → (◡𝐺 ↾ 𝐵) Isom < , E (𝐵, 𝐶)) |
20 | 11, 12, 19 | sylancr 694 |
. . . . . . . 8
⊢
((#‘𝐴) ∈
ℕ0 → (◡𝐺 ↾ 𝐵) Isom < , E (𝐵, 𝐶)) |
21 | 2, 20 | syl 17 |
. . . . . . 7
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (◡𝐺 ↾ 𝐵) Isom < , E (𝐵, 𝐶)) |
22 | | nnz 11276 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ ℕ → 𝑓 ∈
ℤ) |
23 | 2 | nn0zd 11356 |
. . . . . . . . . . . . 13
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (#‘𝐴) ∈
ℤ) |
24 | | eluz 11577 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ ℤ ∧
(#‘𝐴) ∈ ℤ)
→ ((#‘𝐴) ∈
(ℤ≥‘𝑓) ↔ 𝑓 ≤ (#‘𝐴))) |
25 | 22, 23, 24 | syl2anr 494 |
. . . . . . . . . . . 12
⊢ (((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → ((#‘𝐴) ∈
(ℤ≥‘𝑓) ↔ 𝑓 ≤ (#‘𝐴))) |
26 | | zleltp1 11305 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ ℤ ∧
(#‘𝐴) ∈ ℤ)
→ (𝑓 ≤
(#‘𝐴) ↔ 𝑓 < ((#‘𝐴) + 1))) |
27 | 22, 23, 26 | syl2anr 494 |
. . . . . . . . . . . . 13
⊢ (((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → (𝑓 ≤ (#‘𝐴) ↔ 𝑓 < ((#‘𝐴) + 1))) |
28 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐴) + 1)
∈ V |
29 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑓 ∈ V |
30 | 29 | eliniseg 5413 |
. . . . . . . . . . . . . 14
⊢
(((#‘𝐴) + 1)
∈ V → (𝑓 ∈
(◡ < “ {((#‘𝐴) + 1)}) ↔ 𝑓 < ((#‘𝐴) + 1))) |
31 | 28, 30 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ (◡ < “ {((#‘𝐴) + 1)}) ↔ 𝑓 < ((#‘𝐴) + 1)) |
32 | 27, 31 | syl6bbr 277 |
. . . . . . . . . . . 12
⊢ (((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → (𝑓 ≤ (#‘𝐴) ↔ 𝑓 ∈ (◡ < “ {((#‘𝐴) + 1)}))) |
33 | 25, 32 | bitr2d 268 |
. . . . . . . . . . 11
⊢ (((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → (𝑓 ∈ (◡ < “ {((#‘𝐴) + 1)}) ↔ (#‘𝐴) ∈ (ℤ≥‘𝑓))) |
34 | 33 | pm5.32da 671 |
. . . . . . . . . 10
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ((𝑓 ∈ ℕ ∧ 𝑓 ∈ (◡ < “ {((#‘𝐴) + 1)})) ↔ (𝑓 ∈ ℕ ∧ (#‘𝐴) ∈
(ℤ≥‘𝑓)))) |
35 | 13 | elin2 3763 |
. . . . . . . . . 10
⊢ (𝑓 ∈ 𝐵 ↔ (𝑓 ∈ ℕ ∧ 𝑓 ∈ (◡ < “ {((#‘𝐴) + 1)}))) |
36 | | elfzuzb 12207 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (1...(#‘𝐴)) ↔ (𝑓 ∈ (ℤ≥‘1)
∧ (#‘𝐴) ∈
(ℤ≥‘𝑓))) |
37 | | elnnuz 11600 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ ℕ ↔ 𝑓 ∈
(ℤ≥‘1)) |
38 | 37 | anbi1i 727 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ ℕ ∧
(#‘𝐴) ∈
(ℤ≥‘𝑓)) ↔ (𝑓 ∈ (ℤ≥‘1)
∧ (#‘𝐴) ∈
(ℤ≥‘𝑓))) |
39 | 36, 38 | bitr4i 266 |
. . . . . . . . . 10
⊢ (𝑓 ∈ (1...(#‘𝐴)) ↔ (𝑓 ∈ ℕ ∧ (#‘𝐴) ∈
(ℤ≥‘𝑓))) |
40 | 34, 35, 39 | 3bitr4g 302 |
. . . . . . . . 9
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (𝑓 ∈ 𝐵 ↔ 𝑓 ∈ (1...(#‘𝐴)))) |
41 | 40 | eqrdv 2608 |
. . . . . . . 8
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝐵 = (1...(#‘𝐴))) |
42 | | isoeq4 6470 |
. . . . . . . 8
⊢ (𝐵 = (1...(#‘𝐴)) → ((◡𝐺 ↾ 𝐵) Isom < , E (𝐵, 𝐶) ↔ (◡𝐺 ↾ 𝐵) Isom < , E ((1...(#‘𝐴)), 𝐶))) |
43 | 41, 42 | syl 17 |
. . . . . . 7
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ((◡𝐺 ↾ 𝐵) Isom < , E (𝐵, 𝐶) ↔ (◡𝐺 ↾ 𝐵) Isom < , E ((1...(#‘𝐴)), 𝐶))) |
44 | 21, 43 | mpbid 221 |
. . . . . 6
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (◡𝐺 ↾ 𝐵) Isom < , E ((1...(#‘𝐴)), 𝐶)) |
45 | | fz1iso.4 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑂 = OrdIso(𝑅, 𝐴) |
46 | 45 | oion 8324 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ Fin → dom 𝑂 ∈ On) |
47 | 46 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom 𝑂 ∈ On) |
48 | | simpr 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝐴 ∈ Fin) |
49 | | wofi 8094 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝑅 We 𝐴) |
50 | 45 | oien 8326 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ Fin ∧ 𝑅 We 𝐴) → dom 𝑂 ≈ 𝐴) |
51 | 48, 49, 50 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom 𝑂 ≈ 𝐴) |
52 | | enfii 8062 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ Fin ∧ dom 𝑂 ≈ 𝐴) → dom 𝑂 ∈ Fin) |
53 | 48, 51, 52 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom 𝑂 ∈ Fin) |
54 | 47, 53 | elind 3760 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom 𝑂 ∈ (On ∩ Fin)) |
55 | | onfin2 8037 |
. . . . . . . . . . . . . . 15
⊢ ω =
(On ∩ Fin) |
56 | 54, 55 | syl6eleqr 2699 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom 𝑂 ∈ ω) |
57 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢
(rec((𝑛 ∈ V
↦ (𝑛 + 1)), 0)
↾ ω) = (rec((𝑛
∈ V ↦ (𝑛 + 1)),
0) ↾ ω) |
58 | | 0z 11265 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℤ |
59 | 5, 57, 4, 58 | uzrdgxfr 12628 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝑂 ∈ ω →
(𝐺‘dom 𝑂) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + (1 −
0))) |
60 | | 1m0e1 11008 |
. . . . . . . . . . . . . . . 16
⊢ (1
− 0) = 1 |
61 | 60 | oveq2i 6560 |
. . . . . . . . . . . . . . 15
⊢
(((rec((𝑛 ∈ V
↦ (𝑛 + 1)), 0)
↾ ω)‘dom 𝑂) + (1 − 0)) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾
ω)‘dom 𝑂) +
1) |
62 | 59, 61 | syl6eq 2660 |
. . . . . . . . . . . . . 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 7893 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝐴 ≈ dom 𝑂) |
65 | | cardennn 8692 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ≈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → (card‘𝐴) = dom 𝑂) |
66 | 64, 56, 65 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (card‘𝐴) = dom 𝑂) |
67 | 66 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾
ω)‘(card‘𝐴)) = ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂)) |
68 | 57 | hashgval 12982 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ Fin → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾
ω)‘(card‘𝐴)) = (#‘𝐴)) |
69 | 68 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾
ω)‘(card‘𝐴)) = (#‘𝐴)) |
70 | 67, 69 | eqtr3d 2646 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾
ω)‘dom 𝑂) =
(#‘𝐴)) |
71 | 70 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾
ω)‘dom 𝑂) + 1)
= ((#‘𝐴) +
1)) |
72 | 63, 71 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (𝐺‘dom 𝑂) = ((#‘𝐴) + 1)) |
73 | 72 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (◡𝐺‘(𝐺‘dom 𝑂)) = (◡𝐺‘((#‘𝐴) + 1))) |
74 | | isof1o 6473 |
. . . . . . . . . . . . 13
⊢ (𝐺 Isom E , < (ω,
ℕ) → 𝐺:ω–1-1-onto→ℕ) |
75 | 9, 74 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ 𝐺:ω–1-1-onto→ℕ |
76 | | f1ocnvfv1 6432 |
. . . . . . . . . . . 12
⊢ ((𝐺:ω–1-1-onto→ℕ ∧ dom 𝑂 ∈ ω) → (◡𝐺‘(𝐺‘dom 𝑂)) = dom 𝑂) |
77 | 75, 56, 76 | sylancr 694 |
. . . . . . . . . . 11
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (◡𝐺‘(𝐺‘dom 𝑂)) = dom 𝑂) |
78 | 73, 77 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (◡𝐺‘((#‘𝐴) + 1)) = dom 𝑂) |
79 | 78 | ineq2d 3776 |
. . . . . . . . 9
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (ω ∩ (◡𝐺‘((#‘𝐴) + 1))) = (ω ∩ dom 𝑂)) |
80 | | ordom 6966 |
. . . . . . . . . . 11
⊢ Ord
ω |
81 | | ordelss 5656 |
. . . . . . . . . . 11
⊢ ((Ord
ω ∧ dom 𝑂 ∈
ω) → dom 𝑂
⊆ ω) |
82 | 80, 56, 81 | sylancr 694 |
. . . . . . . . . 10
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom 𝑂 ⊆ ω) |
83 | | sseqin2 3779 |
. . . . . . . . . 10
⊢ (dom
𝑂 ⊆ ω ↔
(ω ∩ dom 𝑂) = dom
𝑂) |
84 | 82, 83 | sylib 207 |
. . . . . . . . 9
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (ω ∩ dom 𝑂) = dom 𝑂) |
85 | 79, 84 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (ω ∩ (◡𝐺‘((#‘𝐴) + 1))) = dom 𝑂) |
86 | 14, 85 | syl5eq 2656 |
. . . . . . 7
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝐶 = dom 𝑂) |
87 | | isoeq5 6471 |
. . . . . . 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 221 |
. . . . 5
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (◡𝐺 ↾ 𝐵) Isom < , E ((1...(#‘𝐴)), dom 𝑂)) |
90 | 45 | oiiso 8325 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝑅 We 𝐴) → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴)) |
91 | 48, 49, 90 | syl2anc 691 |
. . . . 5
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴)) |
92 | | isotr 6486 |
. . . . 5
⊢ (((◡𝐺 ↾ 𝐵) Isom < , E ((1...(#‘𝐴)), dom 𝑂) ∧ 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴)) → (𝑂 ∘ (◡𝐺 ↾ 𝐵)) Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴)) |
93 | 89, 91, 92 | syl2anc 691 |
. . . 4
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (𝑂 ∘ (◡𝐺 ↾ 𝐵)) Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴)) |
94 | | isof1o 6473 |
. . . 4
⊢ ((𝑂 ∘ (◡𝐺 ↾ 𝐵)) Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴) → (𝑂 ∘ (◡𝐺 ↾ 𝐵)):(1...(#‘𝐴))–1-1-onto→𝐴) |
95 | | f1of 6050 |
. . . 4
⊢ ((𝑂 ∘ (◡𝐺 ↾ 𝐵)):(1...(#‘𝐴))–1-1-onto→𝐴 → (𝑂 ∘ (◡𝐺 ↾ 𝐵)):(1...(#‘𝐴))⟶𝐴) |
96 | 93, 94, 95 | 3syl 18 |
. . 3
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (𝑂 ∘ (◡𝐺 ↾ 𝐵)):(1...(#‘𝐴))⟶𝐴) |
97 | | fzfid 12634 |
. . 3
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (1...(#‘𝐴)) ∈ Fin) |
98 | | fex 6394 |
. . 3
⊢ (((𝑂 ∘ (◡𝐺 ↾ 𝐵)):(1...(#‘𝐴))⟶𝐴 ∧ (1...(#‘𝐴)) ∈ Fin) → (𝑂 ∘ (◡𝐺 ↾ 𝐵)) ∈ V) |
99 | 96, 97, 98 | syl2anc 691 |
. 2
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (𝑂 ∘ (◡𝐺 ↾ 𝐵)) ∈ V) |
100 | | isoeq1 6467 |
. . 3
⊢ (𝑓 = (𝑂 ∘ (◡𝐺 ↾ 𝐵)) → (𝑓 Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴) ↔ (𝑂 ∘ (◡𝐺 ↾ 𝐵)) Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴))) |
101 | 100 | spcegv 3267 |
. 2
⊢ ((𝑂 ∘ (◡𝐺 ↾ 𝐵)) ∈ V → ((𝑂 ∘ (◡𝐺 ↾ 𝐵)) Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴) → ∃𝑓 𝑓 Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴))) |
102 | 99, 93, 101 | sylc 63 |
1
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ∃𝑓 𝑓 Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴)) |