Metamath Proof Explorer

Theorem fz1isolem

Description: Lemma for fz1iso . (Contributed by Mario Carneiro, 2-Apr-2014)

Ref Expression
Hypotheses fz1iso.1 ⊢ 𝐺 = ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω )
fz1iso.2 ⊢ 𝐵 = ( ℕ ∩ ( ◡ < “ { ( ( ♯ ‘ 𝐴 ) + 1 ) } ) )
fz1iso.3 ⊢ 𝐶 = ( ω ∩ ( ◡ 𝐺 ‘ ( ( ♯ ‘ 𝐴 ) + 1 ) ) )
fz1iso.4 ⊢ 𝑂 = OrdIso ( 𝑅 , 𝐴 )
Assertion fz1isolem ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ∃ 𝑓 𝑓 Isom < , 𝑅 ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )

Proof

Step Hyp Ref Expression
1 fz1iso.1 ⊢ 𝐺 = ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 1 ) ↾ ω )
2 fz1iso.2 ⊢ 𝐵 = ( ℕ ∩ ( ◡ < “ { ( ( ♯ ‘ 𝐴 ) + 1 ) } ) )
3 fz1iso.3 ⊢ 𝐶 = ( ω ∩ ( ◡ 𝐺 ‘ ( ( ♯ ‘ 𝐴 ) + 1 ) ) )
4 fz1iso.4 ⊢ 𝑂 = OrdIso ( 𝑅 , 𝐴 )
5 hashcl ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
6 5 adantl ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
7 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
8 1z ⊢ 1 ∈ ℤ
9 8 1 om2uzisoi ⊢ 𝐺 Isom E , < ( ω , ( ℤ≥ ‘ 1 ) )
10 isoeq5 ⊢ ( ℕ = ( ℤ≥ ‘ 1 ) → ( 𝐺 Isom E , < ( ω , ℕ ) ↔ 𝐺 Isom E , < ( ω , ( ℤ≥ ‘ 1 ) ) ) )
11 9 10 mpbiri ⊢ ( ℕ = ( ℤ≥ ‘ 1 ) → 𝐺 Isom E , < ( ω , ℕ ) )
12 7 11 ax-mp ⊢ 𝐺 Isom E , < ( ω , ℕ )
13 isocnv ⊢ ( 𝐺 Isom E , < ( ω , ℕ ) → ◡ 𝐺 Isom < , E ( ℕ , ω ) )
14 12 13 ax-mp ⊢ ◡ 𝐺 Isom < , E ( ℕ , ω )
15 nn0p1nn ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ( ♯ ‘ 𝐴 ) + 1 ) ∈ ℕ )
16 fvex ⊢ ( ◡ 𝐺 ‘ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ∈ V
17 16 epini ⊢ ( ◡ E “ { ( ◡ 𝐺 ‘ ( ( ♯ ‘ 𝐴 ) + 1 ) ) } ) = ( ◡ 𝐺 ‘ ( ( ♯ ‘ 𝐴 ) + 1 ) )
18 17 ineq2i ⊢ ( ω ∩ ( ◡ E “ { ( ◡ 𝐺 ‘ ( ( ♯ ‘ 𝐴 ) + 1 ) ) } ) ) = ( ω ∩ ( ◡ 𝐺 ‘ ( ( ♯ ‘ 𝐴 ) + 1 ) ) )
19 3 18 eqtr4i ⊢ 𝐶 = ( ω ∩ ( ◡ E “ { ( ◡ 𝐺 ‘ ( ( ♯ ‘ 𝐴 ) + 1 ) ) } ) )
20 2 19 isoini2 ⊢ ( ( ◡ 𝐺 Isom < , E ( ℕ , ω ) ∧ ( ( ♯ ‘ 𝐴 ) + 1 ) ∈ ℕ ) → ( ◡ 𝐺 ↾ 𝐵 ) Isom < , E ( 𝐵 , 𝐶 ) )
21 14 15 20 sylancr ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ◡ 𝐺 ↾ 𝐵 ) Isom < , E ( 𝐵 , 𝐶 ) )
22 6 21 syl ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( ◡ 𝐺 ↾ 𝐵 ) Isom < , E ( 𝐵 , 𝐶 ) )
23 nnz ⊢ ( 𝑓 ∈ ℕ → 𝑓 ∈ ℤ )
24 6 nn0zd ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( ♯ ‘ 𝐴 ) ∈ ℤ )
25 eluz ⊢ ( ( 𝑓 ∈ ℤ ∧ ( ♯ ‘ 𝐴 ) ∈ ℤ ) → ( ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝑓 ) ↔ 𝑓 ≤ ( ♯ ‘ 𝐴 ) ) )
26 23 24 25 syl2anr ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) ∧ 𝑓 ∈ ℕ ) → ( ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝑓 ) ↔ 𝑓 ≤ ( ♯ ‘ 𝐴 ) ) )
27 zleltp1 ⊢ ( ( 𝑓 ∈ ℤ ∧ ( ♯ ‘ 𝐴 ) ∈ ℤ ) → ( 𝑓 ≤ ( ♯ ‘ 𝐴 ) ↔ 𝑓 < ( ( ♯ ‘ 𝐴 ) + 1 ) ) )
28 23 24 27 syl2anr ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) ∧ 𝑓 ∈ ℕ ) → ( 𝑓 ≤ ( ♯ ‘ 𝐴 ) ↔ 𝑓 < ( ( ♯ ‘ 𝐴 ) + 1 ) ) )
29 ovex ⊢ ( ( ♯ ‘ 𝐴 ) + 1 ) ∈ V
30 vex ⊢ 𝑓 ∈ V
31 30 eliniseg ⊢ ( ( ( ♯ ‘ 𝐴 ) + 1 ) ∈ V → ( 𝑓 ∈ ( ◡ < “ { ( ( ♯ ‘ 𝐴 ) + 1 ) } ) ↔ 𝑓 < ( ( ♯ ‘ 𝐴 ) + 1 ) ) )
32 29 31 ax-mp ⊢ ( 𝑓 ∈ ( ◡ < “ { ( ( ♯ ‘ 𝐴 ) + 1 ) } ) ↔ 𝑓 < ( ( ♯ ‘ 𝐴 ) + 1 ) )
33 28 32 bitr4di ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) ∧ 𝑓 ∈ ℕ ) → ( 𝑓 ≤ ( ♯ ‘ 𝐴 ) ↔ 𝑓 ∈ ( ◡ < “ { ( ( ♯ ‘ 𝐴 ) + 1 ) } ) ) )
34 26 33 bitr2d ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) ∧ 𝑓 ∈ ℕ ) → ( 𝑓 ∈ ( ◡ < “ { ( ( ♯ ‘ 𝐴 ) + 1 ) } ) ↔ ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝑓 ) ) )
35 34 pm5.32da ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( ( 𝑓 ∈ ℕ ∧ 𝑓 ∈ ( ◡ < “ { ( ( ♯ ‘ 𝐴 ) + 1 ) } ) ) ↔ ( 𝑓 ∈ ℕ ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝑓 ) ) ) )
36 2 elin2 ⊢ ( 𝑓 ∈ 𝐵 ↔ ( 𝑓 ∈ ℕ ∧ 𝑓 ∈ ( ◡ < “ { ( ( ♯ ‘ 𝐴 ) + 1 ) } ) ) )
37 elfzuzb ⊢ ( 𝑓 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ↔ ( 𝑓 ∈ ( ℤ≥ ‘ 1 ) ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝑓 ) ) )
38 elnnuz ⊢ ( 𝑓 ∈ ℕ ↔ 𝑓 ∈ ( ℤ≥ ‘ 1 ) )
39 38 anbi1i ⊢ ( ( 𝑓 ∈ ℕ ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝑓 ) ) ↔ ( 𝑓 ∈ ( ℤ≥ ‘ 1 ) ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝑓 ) ) )
40 37 39 bitr4i ⊢ ( 𝑓 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ↔ ( 𝑓 ∈ ℕ ∧ ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝑓 ) ) )
41 35 36 40 3bitr4g ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝑓 ∈ 𝐵 ↔ 𝑓 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) )
42 41 eqrdv ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → 𝐵 = ( 1 ... ( ♯ ‘ 𝐴 ) ) )
43 isoeq4 ⊢ ( 𝐵 = ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( ( ◡ 𝐺 ↾ 𝐵 ) Isom < , E ( 𝐵 , 𝐶 ) ↔ ( ◡ 𝐺 ↾ 𝐵 ) Isom < , E ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐶 ) ) )
44 42 43 syl ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( ( ◡ 𝐺 ↾ 𝐵 ) Isom < , E ( 𝐵 , 𝐶 ) ↔ ( ◡ 𝐺 ↾ 𝐵 ) Isom < , E ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐶 ) ) )
45 22 44 mpbid ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( ◡ 𝐺 ↾ 𝐵 ) Isom < , E ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐶 ) )
46 4 oion ⊢ ( 𝐴 ∈ Fin → dom 𝑂 ∈ On )
47 46 adantl ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → dom 𝑂 ∈ On )
48 simpr ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → 𝐴 ∈ Fin )
49 wofi ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → 𝑅 We 𝐴 )
50 4 oien ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑅 We 𝐴 ) → dom 𝑂 ≈ 𝐴 )
51 48 49 50 syl2anc ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → dom 𝑂 ≈ 𝐴 )
52 enfii ⊢ ( ( 𝐴 ∈ Fin ∧ dom 𝑂 ≈ 𝐴 ) → dom 𝑂 ∈ Fin )
53 48 51 52 syl2anc ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → dom 𝑂 ∈ Fin )
54 47 53 elind ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → dom 𝑂 ∈ ( On ∩ Fin ) )
55 onfin2 ⊢ ω = ( On ∩ Fin )
56 54 55 eleqtrrdi ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → dom 𝑂 ∈ ω )
57 eqid ⊢ ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 0 ) ↾ ω ) = ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 0 ) ↾ ω )
58 0z ⊢ 0 ∈ ℤ
59 1 57 8 58 uzrdgxfr ⊢ ( dom 𝑂 ∈ ω → ( 𝐺 ‘ dom 𝑂 ) = ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 0 ) ↾ ω ) ‘ dom 𝑂 ) + ( 1 − 0 ) ) )
60 1m0e1 ⊢ ( 1 − 0 ) = 1
61 60 oveq2i ⊢ ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 0 ) ↾ ω ) ‘ dom 𝑂 ) + ( 1 − 0 ) ) = ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 0 ) ↾ ω ) ‘ dom 𝑂 ) + 1 )
62 59 61 eqtrdi ⊢ ( dom 𝑂 ∈ ω → ( 𝐺 ‘ dom 𝑂 ) = ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 0 ) ↾ ω ) ‘ dom 𝑂 ) + 1 ) )
63 56 62 syl ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝐺 ‘ dom 𝑂 ) = ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 0 ) ↾ ω ) ‘ dom 𝑂 ) + 1 ) )
64 51 ensymd ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → 𝐴 ≈ dom 𝑂 )
65 cardennn ⊢ ( ( 𝐴 ≈ dom 𝑂 ∧ dom 𝑂 ∈ ω ) → ( card ‘ 𝐴 ) = dom 𝑂 )
66 64 56 65 syl2anc ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( card ‘ 𝐴 ) = dom 𝑂 )
67 66 fveq2d ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) = ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 0 ) ↾ ω ) ‘ dom 𝑂 ) )
68 57 hashgval ⊢ ( 𝐴 ∈ Fin → ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) )
69 68 adantl ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) )
70 67 69 eqtr3d ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 0 ) ↾ ω ) ‘ dom 𝑂 ) = ( ♯ ‘ 𝐴 ) )
71 70 oveq1d ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( ( ( rec ( ( 𝑛 ∈ V ↦ ( 𝑛 + 1 ) ) , 0 ) ↾ ω ) ‘ dom 𝑂 ) + 1 ) = ( ( ♯ ‘ 𝐴 ) + 1 ) )
72 63 71 eqtrd ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝐺 ‘ dom 𝑂 ) = ( ( ♯ ‘ 𝐴 ) + 1 ) )
73 72 fveq2d ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( ◡ 𝐺 ‘ ( 𝐺 ‘ dom 𝑂 ) ) = ( ◡ 𝐺 ‘ ( ( ♯ ‘ 𝐴 ) + 1 ) ) )
74 isof1o ⊢ ( 𝐺 Isom E , < ( ω , ℕ ) → 𝐺 : ω –1-1-onto→ ℕ )
75 12 74 ax-mp ⊢ 𝐺 : ω –1-1-onto→ ℕ
76 f1ocnvfv1 ⊢ ( ( 𝐺 : ω –1-1-onto→ ℕ ∧ dom 𝑂 ∈ ω ) → ( ◡ 𝐺 ‘ ( 𝐺 ‘ dom 𝑂 ) ) = dom 𝑂 )
77 75 56 76 sylancr ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( ◡ 𝐺 ‘ ( 𝐺 ‘ dom 𝑂 ) ) = dom 𝑂 )
78 73 77 eqtr3d ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( ◡ 𝐺 ‘ ( ( ♯ ‘ 𝐴 ) + 1 ) ) = dom 𝑂 )
79 78 ineq2d ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( ω ∩ ( ◡ 𝐺 ‘ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) = ( ω ∩ dom 𝑂 ) )
80 ordom ⊢ Ord ω
81 ordelss ⊢ ( ( Ord ω ∧ dom 𝑂 ∈ ω ) → dom 𝑂 ⊆ ω )
82 80 56 81 sylancr ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → dom 𝑂 ⊆ ω )
83 sseqin2 ⊢ ( dom 𝑂 ⊆ ω ↔ ( ω ∩ dom 𝑂 ) = dom 𝑂 )
84 82 83 sylib ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( ω ∩ dom 𝑂 ) = dom 𝑂 )
85 79 84 eqtrd ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( ω ∩ ( ◡ 𝐺 ‘ ( ( ♯ ‘ 𝐴 ) + 1 ) ) ) = dom 𝑂 )
86 3 85 syl5eq ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → 𝐶 = dom 𝑂 )
87 isoeq5 ⊢ ( 𝐶 = dom 𝑂 → ( ( ◡ 𝐺 ↾ 𝐵 ) Isom < , E ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐶 ) ↔ ( ◡ 𝐺 ↾ 𝐵 ) Isom < , E ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , dom 𝑂 ) ) )
88 86 87 syl ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( ( ◡ 𝐺 ↾ 𝐵 ) Isom < , E ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐶 ) ↔ ( ◡ 𝐺 ↾ 𝐵 ) Isom < , E ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , dom 𝑂 ) ) )
89 45 88 mpbid ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( ◡ 𝐺 ↾ 𝐵 ) Isom < , E ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , dom 𝑂 ) )
90 4 oiiso ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑅 We 𝐴 ) → 𝑂 Isom E , 𝑅 ( dom 𝑂 , 𝐴 ) )
91 48 49 90 syl2anc ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → 𝑂 Isom E , 𝑅 ( dom 𝑂 , 𝐴 ) )
92 isotr ⊢ ( ( ( ◡ 𝐺 ↾ 𝐵 ) Isom < , E ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , dom 𝑂 ) ∧ 𝑂 Isom E , 𝑅 ( dom 𝑂 , 𝐴 ) ) → ( 𝑂 ∘ ( ◡ 𝐺 ↾ 𝐵 ) ) Isom < , 𝑅 ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )
93 89 91 92 syl2anc ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝑂 ∘ ( ◡ 𝐺 ↾ 𝐵 ) ) Isom < , 𝑅 ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )
94 isof1o ⊢ ( ( 𝑂 ∘ ( ◡ 𝐺 ↾ 𝐵 ) ) Isom < , 𝑅 ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) → ( 𝑂 ∘ ( ◡ 𝐺 ↾ 𝐵 ) ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 )
95 f1of ⊢ ( ( 𝑂 ∘ ( ◡ 𝐺 ↾ 𝐵 ) ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ 𝐴 → ( 𝑂 ∘ ( ◡ 𝐺 ↾ 𝐵 ) ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
96 93 94 95 3syl ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝑂 ∘ ( ◡ 𝐺 ↾ 𝐵 ) ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) ⟶ 𝐴 )
97 fzfid ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( 1 ... ( ♯ ‘ 𝐴 ) ) ∈ Fin )
98 96 97 fexd ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝑂 ∘ ( ◡ 𝐺 ↾ 𝐵 ) ) ∈ V )
99 isoeq1 ⊢ ( 𝑓 = ( 𝑂 ∘ ( ◡ 𝐺 ↾ 𝐵 ) ) → ( 𝑓 Isom < , 𝑅 ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ↔ ( 𝑂 ∘ ( ◡ 𝐺 ↾ 𝐵 ) ) Isom < , 𝑅 ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) ) )
100 98 93 99 spcedv ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ∃ 𝑓 𝑓 Isom < , 𝑅 ( ( 1 ... ( ♯ ‘ 𝐴 ) ) , 𝐴 ) )