Proof of Theorem fz1isolem
| Step | Hyp | Ref
| Expression |
| 1 | | hashcl 14395 |
. . . . . . . . 9
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℕ0) |
| 2 | 1 | adantl 481 |
. . . . . . . 8
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (♯‘𝐴) ∈
ℕ0) |
| 3 | | nnuz 12921 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
| 4 | | 1z 12647 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℤ |
| 5 | | fz1iso.1 |
. . . . . . . . . . . . 13
⊢ 𝐺 = (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω) |
| 6 | 4, 5 | om2uzisoi 13995 |
. . . . . . . . . . . 12
⊢ 𝐺 Isom E , < (ω,
(ℤ≥‘1)) |
| 7 | | isoeq5 7341 |
. . . . . . . . . . . 12
⊢ (ℕ
= (ℤ≥‘1) → (𝐺 Isom E , < (ω, ℕ) ↔
𝐺 Isom E , < (ω,
(ℤ≥‘1)))) |
| 8 | 6, 7 | mpbiri 258 |
. . . . . . . . . . 11
⊢ (ℕ
= (ℤ≥‘1) → 𝐺 Isom E , < (ω,
ℕ)) |
| 9 | 3, 8 | ax-mp 5 |
. . . . . . . . . 10
⊢ 𝐺 Isom E , < (ω,
ℕ) |
| 10 | | isocnv 7350 |
. . . . . . . . . 10
⊢ (𝐺 Isom E , < (ω,
ℕ) → ◡𝐺 Isom < , E (ℕ,
ω)) |
| 11 | 9, 10 | ax-mp 5 |
. . . . . . . . 9
⊢ ◡𝐺 Isom < , E (ℕ,
ω) |
| 12 | | nn0p1nn 12565 |
. . . . . . . . 9
⊢
((♯‘𝐴)
∈ ℕ0 → ((♯‘𝐴) + 1) ∈ ℕ) |
| 13 | | fz1iso.2 |
. . . . . . . . . 10
⊢ 𝐵 = (ℕ ∩ (◡ < “ {((♯‘𝐴) + 1)})) |
| 14 | | fz1iso.3 |
. . . . . . . . . . 11
⊢ 𝐶 = (ω ∩ (◡𝐺‘((♯‘𝐴) + 1))) |
| 15 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢ (◡𝐺‘((♯‘𝐴) + 1)) ∈ V |
| 16 | 15 | epini 6114 |
. . . . . . . . . . . 12
⊢ (◡ E “ {(◡𝐺‘((♯‘𝐴) + 1))}) = (◡𝐺‘((♯‘𝐴) + 1)) |
| 17 | 16 | ineq2i 4217 |
. . . . . . . . . . 11
⊢ (ω
∩ (◡ E “ {(◡𝐺‘((♯‘𝐴) + 1))})) = (ω ∩ (◡𝐺‘((♯‘𝐴) + 1))) |
| 18 | 14, 17 | eqtr4i 2768 |
. . . . . . . . . 10
⊢ 𝐶 = (ω ∩ (◡ E “ {(◡𝐺‘((♯‘𝐴) + 1))})) |
| 19 | 13, 18 | isoini2 7359 |
. . . . . . . . 9
⊢ ((◡𝐺 Isom < , E (ℕ, ω) ∧
((♯‘𝐴) + 1)
∈ ℕ) → (◡𝐺 ↾ 𝐵) Isom < , E (𝐵, 𝐶)) |
| 20 | 11, 12, 19 | sylancr 587 |
. . . . . . . 8
⊢
((♯‘𝐴)
∈ ℕ0 → (◡𝐺 ↾ 𝐵) Isom < , E (𝐵, 𝐶)) |
| 21 | 2, 20 | syl 17 |
. . . . . . 7
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (◡𝐺 ↾ 𝐵) Isom < , E (𝐵, 𝐶)) |
| 22 | | nnz 12634 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ ℕ → 𝑓 ∈
ℤ) |
| 23 | 2 | nn0zd 12639 |
. . . . . . . . . . . . 13
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (♯‘𝐴) ∈
ℤ) |
| 24 | | eluz 12892 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ ℤ ∧
(♯‘𝐴) ∈
ℤ) → ((♯‘𝐴) ∈ (ℤ≥‘𝑓) ↔ 𝑓 ≤ (♯‘𝐴))) |
| 25 | 22, 23, 24 | syl2anr 597 |
. . . . . . . . . . . 12
⊢ (((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → ((♯‘𝐴) ∈
(ℤ≥‘𝑓) ↔ 𝑓 ≤ (♯‘𝐴))) |
| 26 | | zleltp1 12668 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ ℤ ∧
(♯‘𝐴) ∈
ℤ) → (𝑓 ≤
(♯‘𝐴) ↔
𝑓 <
((♯‘𝐴) +
1))) |
| 27 | 22, 23, 26 | syl2anr 597 |
. . . . . . . . . . . . 13
⊢ (((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → (𝑓 ≤ (♯‘𝐴) ↔ 𝑓 < ((♯‘𝐴) + 1))) |
| 28 | | ovex 7464 |
. . . . . . . . . . . . . 14
⊢
((♯‘𝐴) +
1) ∈ V |
| 29 | | vex 3484 |
. . . . . . . . . . . . . . 15
⊢ 𝑓 ∈ V |
| 30 | 29 | eliniseg 6112 |
. . . . . . . . . . . . . 14
⊢
(((♯‘𝐴)
+ 1) ∈ V → (𝑓
∈ (◡ < “
{((♯‘𝐴) + 1)})
↔ 𝑓 <
((♯‘𝐴) +
1))) |
| 31 | 28, 30 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ (◡ < “ {((♯‘𝐴) + 1)}) ↔ 𝑓 < ((♯‘𝐴) + 1)) |
| 32 | 27, 31 | bitr4di 289 |
. . . . . . . . . . . 12
⊢ (((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → (𝑓 ≤ (♯‘𝐴) ↔ 𝑓 ∈ (◡ < “ {((♯‘𝐴) + 1)}))) |
| 33 | 25, 32 | bitr2d 280 |
. . . . . . . . . . 11
⊢ (((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → (𝑓 ∈ (◡ < “ {((♯‘𝐴) + 1)}) ↔
(♯‘𝐴) ∈
(ℤ≥‘𝑓))) |
| 34 | 33 | pm5.32da 579 |
. . . . . . . . . 10
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ((𝑓 ∈ ℕ ∧ 𝑓 ∈ (◡ < “ {((♯‘𝐴) + 1)})) ↔ (𝑓 ∈ ℕ ∧
(♯‘𝐴) ∈
(ℤ≥‘𝑓)))) |
| 35 | 13 | elin2 4203 |
. . . . . . . . . 10
⊢ (𝑓 ∈ 𝐵 ↔ (𝑓 ∈ ℕ ∧ 𝑓 ∈ (◡ < “ {((♯‘𝐴) + 1)}))) |
| 36 | | elfzuzb 13558 |
. . . . . . . . . . 11
⊢ (𝑓 ∈
(1...(♯‘𝐴))
↔ (𝑓 ∈
(ℤ≥‘1) ∧ (♯‘𝐴) ∈ (ℤ≥‘𝑓))) |
| 37 | | elnnuz 12922 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ ℕ ↔ 𝑓 ∈
(ℤ≥‘1)) |
| 38 | 37 | anbi1i 624 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ ℕ ∧
(♯‘𝐴) ∈
(ℤ≥‘𝑓)) ↔ (𝑓 ∈ (ℤ≥‘1)
∧ (♯‘𝐴)
∈ (ℤ≥‘𝑓))) |
| 39 | 36, 38 | bitr4i 278 |
. . . . . . . . . 10
⊢ (𝑓 ∈
(1...(♯‘𝐴))
↔ (𝑓 ∈ ℕ
∧ (♯‘𝐴)
∈ (ℤ≥‘𝑓))) |
| 40 | 34, 35, 39 | 3bitr4g 314 |
. . . . . . . . 9
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (𝑓 ∈ 𝐵 ↔ 𝑓 ∈ (1...(♯‘𝐴)))) |
| 41 | 40 | eqrdv 2735 |
. . . . . . . 8
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝐵 = (1...(♯‘𝐴))) |
| 42 | | isoeq4 7340 |
. . . . . . . 8
⊢ (𝐵 = (1...(♯‘𝐴)) → ((◡𝐺 ↾ 𝐵) Isom < , E (𝐵, 𝐶) ↔ (◡𝐺 ↾ 𝐵) Isom < , E ((1...(♯‘𝐴)), 𝐶))) |
| 43 | 41, 42 | syl 17 |
. . . . . . 7
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ((◡𝐺 ↾ 𝐵) Isom < , E (𝐵, 𝐶) ↔ (◡𝐺 ↾ 𝐵) Isom < , E ((1...(♯‘𝐴)), 𝐶))) |
| 44 | 21, 43 | mpbid 232 |
. . . . . 6
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (◡𝐺 ↾ 𝐵) Isom < , E ((1...(♯‘𝐴)), 𝐶)) |
| 45 | | fz1iso.4 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑂 = OrdIso(𝑅, 𝐴) |
| 46 | 45 | oion 9576 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ Fin → dom 𝑂 ∈ On) |
| 47 | 46 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom 𝑂 ∈ On) |
| 48 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝐴 ∈ Fin) |
| 49 | | wofi 9325 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝑅 We 𝐴) |
| 50 | 45 | oien 9578 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ Fin ∧ 𝑅 We 𝐴) → dom 𝑂 ≈ 𝐴) |
| 51 | 48, 49, 50 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom 𝑂 ≈ 𝐴) |
| 52 | | enfii 9226 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ Fin ∧ dom 𝑂 ≈ 𝐴) → dom 𝑂 ∈ Fin) |
| 53 | 48, 51, 52 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom 𝑂 ∈ Fin) |
| 54 | 47, 53 | elind 4200 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom 𝑂 ∈ (On ∩ Fin)) |
| 55 | | onfin2 9268 |
. . . . . . . . . . . . . . 15
⊢ ω =
(On ∩ Fin) |
| 56 | 54, 55 | eleqtrrdi 2852 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom 𝑂 ∈ ω) |
| 57 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢
(rec((𝑛 ∈ V
↦ (𝑛 + 1)), 0)
↾ ω) = (rec((𝑛
∈ V ↦ (𝑛 + 1)),
0) ↾ ω) |
| 58 | | 0z 12624 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℤ |
| 59 | 5, 57, 4, 58 | uzrdgxfr 14008 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝑂 ∈ ω →
(𝐺‘dom 𝑂) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + (1 −
0))) |
| 60 | | 1m0e1 12387 |
. . . . . . . . . . . . . . . 16
⊢ (1
− 0) = 1 |
| 61 | 60 | oveq2i 7442 |
. . . . . . . . . . . . . . 15
⊢
(((rec((𝑛 ∈ V
↦ (𝑛 + 1)), 0)
↾ ω)‘dom 𝑂) + (1 − 0)) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾
ω)‘dom 𝑂) +
1) |
| 62 | 59, 61 | eqtrdi 2793 |
. . . . . . . . . . . . . 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 9045 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝐴 ≈ dom 𝑂) |
| 65 | | cardennn 10023 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ≈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → (card‘𝐴) = dom 𝑂) |
| 66 | 64, 56, 65 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (card‘𝐴) = dom 𝑂) |
| 67 | 66 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾
ω)‘(card‘𝐴)) = ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂)) |
| 68 | 57 | hashgval 14372 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ Fin → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾
ω)‘(card‘𝐴)) = (♯‘𝐴)) |
| 69 | 68 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾
ω)‘(card‘𝐴)) = (♯‘𝐴)) |
| 70 | 67, 69 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾
ω)‘dom 𝑂) =
(♯‘𝐴)) |
| 71 | 70 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾
ω)‘dom 𝑂) + 1)
= ((♯‘𝐴) +
1)) |
| 72 | 63, 71 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (𝐺‘dom 𝑂) = ((♯‘𝐴) + 1)) |
| 73 | 72 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (◡𝐺‘(𝐺‘dom 𝑂)) = (◡𝐺‘((♯‘𝐴) + 1))) |
| 74 | | isof1o 7343 |
. . . . . . . . . . . . 13
⊢ (𝐺 Isom E , < (ω,
ℕ) → 𝐺:ω–1-1-onto→ℕ) |
| 75 | 9, 74 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ 𝐺:ω–1-1-onto→ℕ |
| 76 | | f1ocnvfv1 7296 |
. . . . . . . . . . . 12
⊢ ((𝐺:ω–1-1-onto→ℕ ∧ dom 𝑂 ∈ ω) → (◡𝐺‘(𝐺‘dom 𝑂)) = dom 𝑂) |
| 77 | 75, 56, 76 | sylancr 587 |
. . . . . . . . . . 11
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (◡𝐺‘(𝐺‘dom 𝑂)) = dom 𝑂) |
| 78 | 73, 77 | eqtr3d 2779 |
. . . . . . . . . 10
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (◡𝐺‘((♯‘𝐴) + 1)) = dom 𝑂) |
| 79 | 78 | ineq2d 4220 |
. . . . . . . . 9
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (ω ∩ (◡𝐺‘((♯‘𝐴) + 1))) = (ω ∩ dom 𝑂)) |
| 80 | | ordom 7897 |
. . . . . . . . . . 11
⊢ Ord
ω |
| 81 | | ordelss 6400 |
. . . . . . . . . . 11
⊢ ((Ord
ω ∧ dom 𝑂 ∈
ω) → dom 𝑂
⊆ ω) |
| 82 | 80, 56, 81 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom 𝑂 ⊆ ω) |
| 83 | | sseqin2 4223 |
. . . . . . . . . 10
⊢ (dom
𝑂 ⊆ ω ↔
(ω ∩ dom 𝑂) = dom
𝑂) |
| 84 | 82, 83 | sylib 218 |
. . . . . . . . 9
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (ω ∩ dom 𝑂) = dom 𝑂) |
| 85 | 79, 84 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (ω ∩ (◡𝐺‘((♯‘𝐴) + 1))) = dom 𝑂) |
| 86 | 14, 85 | eqtrid 2789 |
. . . . . . 7
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝐶 = dom 𝑂) |
| 87 | | isoeq5 7341 |
. . . . . . 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 232 |
. . . . 5
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (◡𝐺 ↾ 𝐵) Isom < , E ((1...(♯‘𝐴)), dom 𝑂)) |
| 90 | 45 | oiiso 9577 |
. . . . . 6
⊢ ((𝐴 ∈ Fin ∧ 𝑅 We 𝐴) → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴)) |
| 91 | 48, 49, 90 | syl2anc 584 |
. . . . 5
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴)) |
| 92 | | isotr 7356 |
. . . . 5
⊢ (((◡𝐺 ↾ 𝐵) Isom < , E ((1...(♯‘𝐴)), dom 𝑂) ∧ 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴)) → (𝑂 ∘ (◡𝐺 ↾ 𝐵)) Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴)) |
| 93 | 89, 91, 92 | syl2anc 584 |
. . . 4
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (𝑂 ∘ (◡𝐺 ↾ 𝐵)) Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴)) |
| 94 | | isof1o 7343 |
. . . 4
⊢ ((𝑂 ∘ (◡𝐺 ↾ 𝐵)) Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴) → (𝑂 ∘ (◡𝐺 ↾ 𝐵)):(1...(♯‘𝐴))–1-1-onto→𝐴) |
| 95 | | f1of 6848 |
. . . 4
⊢ ((𝑂 ∘ (◡𝐺 ↾ 𝐵)):(1...(♯‘𝐴))–1-1-onto→𝐴 → (𝑂 ∘ (◡𝐺 ↾ 𝐵)):(1...(♯‘𝐴))⟶𝐴) |
| 96 | 93, 94, 95 | 3syl 18 |
. . 3
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (𝑂 ∘ (◡𝐺 ↾ 𝐵)):(1...(♯‘𝐴))⟶𝐴) |
| 97 | | fzfid 14014 |
. . 3
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) →
(1...(♯‘𝐴))
∈ Fin) |
| 98 | 96, 97 | fexd 7247 |
. 2
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (𝑂 ∘ (◡𝐺 ↾ 𝐵)) ∈ V) |
| 99 | | isoeq1 7337 |
. 2
⊢ (𝑓 = (𝑂 ∘ (◡𝐺 ↾ 𝐵)) → (𝑓 Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴) ↔ (𝑂 ∘ (◡𝐺 ↾ 𝐵)) Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴))) |
| 100 | 98, 93, 99 | spcedv 3598 |
1
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ∃𝑓 𝑓 Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴)) |