Metamath Proof Explorer

Theorem erdsze2lem1

Description: Lemma for erdsze2 . (Contributed by Mario Carneiro, 22-Jan-2015)

Ref Expression
Hypotheses erdsze2.r ⊒ ( πœ‘ β†’ 𝑅 ∈ β„• )
erdsze2.s ⊒ ( πœ‘ β†’ 𝑆 ∈ β„• )
erdsze2.f ⊒ ( πœ‘ β†’ 𝐹 : 𝐴 –1-1β†’ ℝ )
erdsze2.a ⊒ ( πœ‘ β†’ 𝐴 βŠ† ℝ )
erdsze2lem.n ⊒ 𝑁 = ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) )
erdsze2lem.l ⊒ ( πœ‘ β†’ 𝑁 < ( β™― β€˜ 𝐴 ) )
Assertion erdsze2lem1 ( πœ‘ β†’ βˆƒ 𝑓 ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1β†’ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( 𝑁 + 1 ) ) , ran 𝑓 ) ) )

Proof

Step Hyp Ref Expression
1 erdsze2.r ⊒ ( πœ‘ β†’ 𝑅 ∈ β„• )
2 erdsze2.s ⊒ ( πœ‘ β†’ 𝑆 ∈ β„• )
3 erdsze2.f ⊒ ( πœ‘ β†’ 𝐹 : 𝐴 –1-1β†’ ℝ )
4 erdsze2.a ⊒ ( πœ‘ β†’ 𝐴 βŠ† ℝ )
5 erdsze2lem.n ⊒ 𝑁 = ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) )
6 erdsze2lem.l ⊒ ( πœ‘ β†’ 𝑁 < ( β™― β€˜ 𝐴 ) )
7 nnm1nn0 ⊒ ( 𝑅 ∈ β„• β†’ ( 𝑅 βˆ’ 1 ) ∈ β„•0 )
8 1 7 syl ⊒ ( πœ‘ β†’ ( 𝑅 βˆ’ 1 ) ∈ β„•0 )
9 nnm1nn0 ⊒ ( 𝑆 ∈ β„• β†’ ( 𝑆 βˆ’ 1 ) ∈ β„•0 )
10 2 9 syl ⊒ ( πœ‘ β†’ ( 𝑆 βˆ’ 1 ) ∈ β„•0 )
11 8 10 nn0mulcld ⊒ ( πœ‘ β†’ ( ( 𝑅 βˆ’ 1 ) Β· ( 𝑆 βˆ’ 1 ) ) ∈ β„•0 )
12 5 11 eqeltrid ⊒ ( πœ‘ β†’ 𝑁 ∈ β„•0 )
13 peano2nn0 ⊒ ( 𝑁 ∈ β„•0 β†’ ( 𝑁 + 1 ) ∈ β„•0 )
14 hashfz1 ⊒ ( ( 𝑁 + 1 ) ∈ β„•0 β†’ ( β™― β€˜ ( 1 ... ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) )
15 12 13 14 3syl ⊒ ( πœ‘ β†’ ( β™― β€˜ ( 1 ... ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) )
16 15 adantr ⊒ ( ( πœ‘ ∧ 𝐴 ∈ Fin ) β†’ ( β™― β€˜ ( 1 ... ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) )
17 6 adantr ⊒ ( ( πœ‘ ∧ 𝐴 ∈ Fin ) β†’ 𝑁 < ( β™― β€˜ 𝐴 ) )
18 hashcl ⊒ ( 𝐴 ∈ Fin β†’ ( β™― β€˜ 𝐴 ) ∈ β„•0 )
19 nn0ltp1le ⊒ ( ( 𝑁 ∈ β„•0 ∧ ( β™― β€˜ 𝐴 ) ∈ β„•0 ) β†’ ( 𝑁 < ( β™― β€˜ 𝐴 ) ↔ ( 𝑁 + 1 ) ≀ ( β™― β€˜ 𝐴 ) ) )
20 12 18 19 syl2an ⊒ ( ( πœ‘ ∧ 𝐴 ∈ Fin ) β†’ ( 𝑁 < ( β™― β€˜ 𝐴 ) ↔ ( 𝑁 + 1 ) ≀ ( β™― β€˜ 𝐴 ) ) )
21 17 20 mpbid ⊒ ( ( πœ‘ ∧ 𝐴 ∈ Fin ) β†’ ( 𝑁 + 1 ) ≀ ( β™― β€˜ 𝐴 ) )
22 16 21 eqbrtrd ⊒ ( ( πœ‘ ∧ 𝐴 ∈ Fin ) β†’ ( β™― β€˜ ( 1 ... ( 𝑁 + 1 ) ) ) ≀ ( β™― β€˜ 𝐴 ) )
23 fzfid ⊒ ( ( πœ‘ ∧ 𝐴 ∈ Fin ) β†’ ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin )
24 simpr ⊒ ( ( πœ‘ ∧ 𝐴 ∈ Fin ) β†’ 𝐴 ∈ Fin )
25 hashdom ⊒ ( ( ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin ∧ 𝐴 ∈ Fin ) β†’ ( ( β™― β€˜ ( 1 ... ( 𝑁 + 1 ) ) ) ≀ ( β™― β€˜ 𝐴 ) ↔ ( 1 ... ( 𝑁 + 1 ) ) β‰Ό 𝐴 ) )
26 23 24 25 syl2anc ⊒ ( ( πœ‘ ∧ 𝐴 ∈ Fin ) β†’ ( ( β™― β€˜ ( 1 ... ( 𝑁 + 1 ) ) ) ≀ ( β™― β€˜ 𝐴 ) ↔ ( 1 ... ( 𝑁 + 1 ) ) β‰Ό 𝐴 ) )
27 22 26 mpbid ⊒ ( ( πœ‘ ∧ 𝐴 ∈ Fin ) β†’ ( 1 ... ( 𝑁 + 1 ) ) β‰Ό 𝐴 )
28 simpr ⊒ ( ( πœ‘ ∧ Β¬ 𝐴 ∈ Fin ) β†’ Β¬ 𝐴 ∈ Fin )
29 fzfid ⊒ ( ( πœ‘ ∧ Β¬ 𝐴 ∈ Fin ) β†’ ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin )
30 isinffi ⊒ ( ( Β¬ 𝐴 ∈ Fin ∧ ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin ) β†’ βˆƒ 𝑓 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1β†’ 𝐴 )
31 28 29 30 syl2anc ⊒ ( ( πœ‘ ∧ Β¬ 𝐴 ∈ Fin ) β†’ βˆƒ 𝑓 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1β†’ 𝐴 )
32 reex ⊒ ℝ ∈ V
33 ssexg ⊒ ( ( 𝐴 βŠ† ℝ ∧ ℝ ∈ V ) β†’ 𝐴 ∈ V )
34 4 32 33 sylancl ⊒ ( πœ‘ β†’ 𝐴 ∈ V )
35 34 adantr ⊒ ( ( πœ‘ ∧ Β¬ 𝐴 ∈ Fin ) β†’ 𝐴 ∈ V )
36 brdomg ⊒ ( 𝐴 ∈ V β†’ ( ( 1 ... ( 𝑁 + 1 ) ) β‰Ό 𝐴 ↔ βˆƒ 𝑓 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1β†’ 𝐴 ) )
37 35 36 syl ⊒ ( ( πœ‘ ∧ Β¬ 𝐴 ∈ Fin ) β†’ ( ( 1 ... ( 𝑁 + 1 ) ) β‰Ό 𝐴 ↔ βˆƒ 𝑓 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1β†’ 𝐴 ) )
38 31 37 mpbird ⊒ ( ( πœ‘ ∧ Β¬ 𝐴 ∈ Fin ) β†’ ( 1 ... ( 𝑁 + 1 ) ) β‰Ό 𝐴 )
39 27 38 pm2.61dan ⊒ ( πœ‘ β†’ ( 1 ... ( 𝑁 + 1 ) ) β‰Ό 𝐴 )
40 domeng ⊒ ( 𝐴 ∈ V β†’ ( ( 1 ... ( 𝑁 + 1 ) ) β‰Ό 𝐴 ↔ βˆƒ 𝑠 ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) )
41 34 40 syl ⊒ ( πœ‘ β†’ ( ( 1 ... ( 𝑁 + 1 ) ) β‰Ό 𝐴 ↔ βˆƒ 𝑠 ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) )
42 39 41 mpbid ⊒ ( πœ‘ β†’ βˆƒ 𝑠 ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) )
43 simprr ⊒ ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) β†’ 𝑠 βŠ† 𝐴 )
44 4 adantr ⊒ ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) β†’ 𝐴 βŠ† ℝ )
45 43 44 sstrd ⊒ ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) β†’ 𝑠 βŠ† ℝ )
46 ltso ⊒ < Or ℝ
47 soss ⊒ ( 𝑠 βŠ† ℝ β†’ ( < Or ℝ β†’ < Or 𝑠 ) )
48 45 46 47 mpisyl ⊒ ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) β†’ < Or 𝑠 )
49 fzfid ⊒ ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) β†’ ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin )
50 simprl ⊒ ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) β†’ ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 )
51 enfi ⊒ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 β†’ ( ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin ↔ 𝑠 ∈ Fin ) )
52 50 51 syl ⊒ ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) β†’ ( ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin ↔ 𝑠 ∈ Fin ) )
53 49 52 mpbid ⊒ ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) β†’ 𝑠 ∈ Fin )
54 fz1iso ⊒ ( ( < Or 𝑠 ∧ 𝑠 ∈ Fin ) β†’ βˆƒ 𝑓 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , 𝑠 ) )
55 48 53 54 syl2anc ⊒ ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) β†’ βˆƒ 𝑓 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , 𝑠 ) )
56 isof1o ⊒ ( 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , 𝑠 ) β†’ 𝑓 : ( 1 ... ( β™― β€˜ 𝑠 ) ) –1-1-ontoβ†’ 𝑠 )
57 56 adantl ⊒ ( ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , 𝑠 ) ) β†’ 𝑓 : ( 1 ... ( β™― β€˜ 𝑠 ) ) –1-1-ontoβ†’ 𝑠 )
58 hashen ⊒ ( ( ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin ∧ 𝑠 ∈ Fin ) β†’ ( ( β™― β€˜ ( 1 ... ( 𝑁 + 1 ) ) ) = ( β™― β€˜ 𝑠 ) ↔ ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ) )
59 49 53 58 syl2anc ⊒ ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) β†’ ( ( β™― β€˜ ( 1 ... ( 𝑁 + 1 ) ) ) = ( β™― β€˜ 𝑠 ) ↔ ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ) )
60 50 59 mpbird ⊒ ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) β†’ ( β™― β€˜ ( 1 ... ( 𝑁 + 1 ) ) ) = ( β™― β€˜ 𝑠 ) )
61 15 adantr ⊒ ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) β†’ ( β™― β€˜ ( 1 ... ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) )
62 60 61 eqtr3d ⊒ ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) β†’ ( β™― β€˜ 𝑠 ) = ( 𝑁 + 1 ) )
63 62 adantr ⊒ ( ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , 𝑠 ) ) β†’ ( β™― β€˜ 𝑠 ) = ( 𝑁 + 1 ) )
64 63 oveq2d ⊒ ( ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , 𝑠 ) ) β†’ ( 1 ... ( β™― β€˜ 𝑠 ) ) = ( 1 ... ( 𝑁 + 1 ) ) )
65 64 f1oeq2d ⊒ ( ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , 𝑠 ) ) β†’ ( 𝑓 : ( 1 ... ( β™― β€˜ 𝑠 ) ) –1-1-ontoβ†’ 𝑠 ↔ 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-ontoβ†’ 𝑠 ) )
66 57 65 mpbid ⊒ ( ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , 𝑠 ) ) β†’ 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-ontoβ†’ 𝑠 )
67 f1of1 ⊒ ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-ontoβ†’ 𝑠 β†’ 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1β†’ 𝑠 )
68 66 67 syl ⊒ ( ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , 𝑠 ) ) β†’ 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1β†’ 𝑠 )
69 simplrr ⊒ ( ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , 𝑠 ) ) β†’ 𝑠 βŠ† 𝐴 )
70 f1ss ⊒ ( ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1β†’ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) β†’ 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1β†’ 𝐴 )
71 68 69 70 syl2anc ⊒ ( ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , 𝑠 ) ) β†’ 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1β†’ 𝐴 )
72 simpr ⊒ ( ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , 𝑠 ) ) β†’ 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , 𝑠 ) )
73 f1ofo ⊒ ( 𝑓 : ( 1 ... ( β™― β€˜ 𝑠 ) ) –1-1-ontoβ†’ 𝑠 β†’ 𝑓 : ( 1 ... ( β™― β€˜ 𝑠 ) ) –ontoβ†’ 𝑠 )
74 forn ⊒ ( 𝑓 : ( 1 ... ( β™― β€˜ 𝑠 ) ) –ontoβ†’ 𝑠 β†’ ran 𝑓 = 𝑠 )
75 isoeq5 ⊒ ( ran 𝑓 = 𝑠 β†’ ( 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , ran 𝑓 ) ↔ 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , 𝑠 ) ) )
76 57 73 74 75 4syl ⊒ ( ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , 𝑠 ) ) β†’ ( 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , ran 𝑓 ) ↔ 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , 𝑠 ) ) )
77 72 76 mpbird ⊒ ( ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , 𝑠 ) ) β†’ 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , ran 𝑓 ) )
78 isoeq4 ⊒ ( ( 1 ... ( β™― β€˜ 𝑠 ) ) = ( 1 ... ( 𝑁 + 1 ) ) β†’ ( 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , ran 𝑓 ) ↔ 𝑓 Isom < , < ( ( 1 ... ( 𝑁 + 1 ) ) , ran 𝑓 ) ) )
79 64 78 syl ⊒ ( ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , 𝑠 ) ) β†’ ( 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , ran 𝑓 ) ↔ 𝑓 Isom < , < ( ( 1 ... ( 𝑁 + 1 ) ) , ran 𝑓 ) ) )
80 77 79 mpbid ⊒ ( ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , 𝑠 ) ) β†’ 𝑓 Isom < , < ( ( 1 ... ( 𝑁 + 1 ) ) , ran 𝑓 ) )
81 71 80 jca ⊒ ( ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , 𝑠 ) ) β†’ ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1β†’ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( 𝑁 + 1 ) ) , ran 𝑓 ) ) )
82 81 ex ⊒ ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) β†’ ( 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , 𝑠 ) β†’ ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1β†’ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( 𝑁 + 1 ) ) , ran 𝑓 ) ) ) )
83 82 eximdv ⊒ ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) β†’ ( βˆƒ 𝑓 𝑓 Isom < , < ( ( 1 ... ( β™― β€˜ 𝑠 ) ) , 𝑠 ) β†’ βˆƒ 𝑓 ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1β†’ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( 𝑁 + 1 ) ) , ran 𝑓 ) ) ) )
84 55 83 mpd ⊒ ( ( πœ‘ ∧ ( ( 1 ... ( 𝑁 + 1 ) ) β‰ˆ 𝑠 ∧ 𝑠 βŠ† 𝐴 ) ) β†’ βˆƒ 𝑓 ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1β†’ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( 𝑁 + 1 ) ) , ran 𝑓 ) ) )
85 42 84 exlimddv ⊒ ( πœ‘ β†’ βˆƒ 𝑓 ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1β†’ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( 𝑁 + 1 ) ) , ran 𝑓 ) ) )